1  /-
  2  Copyright (c) 2019 Seul Baek. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Author: Seul Baek
  5  
  6  Correctness lemmas for equality elimination.
  7  See 5.5 of <http://www.decision-procedures.org/> for details.
  8  -/
  9  
 10  import tactic.omega.clause
src         └─────────────────┘
 11  
 12  open list.func
 13  
 14  namespace omega
 15  
 16  def symdiv (i j : int) : int :=
id                     └─┘    └─┘
src                    └─┘    └─┘
typ                    └─┘    └─┘
 17  if (2 * (i % j)) < j
id                 
src                 
typ                
 18  then i / j
id          
src         
typ         
 19  else (i / j) + 1
id             
src              
typ            
 20  
 21  def symmod (i j : int) : int :=
id                     └─┘    └─┘
src                    └─┘    └─┘
typ                    └─┘    └─┘
 22  if (2 * (i % j)) < j
id                 
src                 
typ                
 23  then i % j
id          
src         
typ         
 24  else (i % j) - j
id              
src              
typ             
 25  
 26  lemma symmod_add_one_self {i : int} :
id                                  └─┘
src                                 └─┘
typ                                 └─┘
 27    0 < i → symmod i (i+1) = -1 :=
id           └────┘       
src           └────┘         
typ          └────┘       
 28  begin
st   └─────
 29    intro h1,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid         └─┘
st   ─────────┘└─
 30    unfold symmod,
src    └───────────┘
typ    └───────────┘
doc    └───────────┘
txt    └───────────┘
par    └───────────┘
pid          └─────┘
st   ──────────────┘└─
 31    rw [int.mod_eq_of_lt (le_of_lt h1) (lt_add_one _), if_neg],
id         └──────────────┘  └──────┘ └┘   └────────┘     └────┘
src    └──┘└──────────────┘ └──────┘  └┘ └────────┘└───┘└────┘
typ    └──┘└──────────────┘ └──────┘└┘└┘ └────────┘└───┘└────┘
doc    └──┘                           └┘           └───┘      
txt    └──┘                           └┘           └───┘      
par    └──┘                           └┘           └───┘      
pid      └┘                           └┘           └───┘      
st   ──────────────────────────────────────────────────┘└──────┘└──
 32    simp only [add_comm, add_neg_cancel_left,
id                └──────┘  └─────────────────┘
src    └─────────┘└──────┘└┘└─────────────────┘└─
typ    └─────────┘└──────┘└┘└─────────────────┘└─
doc    └─────────┘        └┘                   └─
txt    └─────────┘        └┘                   └─
par    └─────────┘        └┘                   └─
pid        └──┘└┘        └┘                   └─
st   ────────────────────────────────────────────
 33      neg_add_rev, sub_eq_add_neg],
id       └─────────┘  └────────────┘
src  ───┘└─────────┘└┘└────────────┘
typ  ───┘└─────────┘└┘└────────────┘
doc  ───┘           └┘              
txt  ───┘           └┘              
par  ───┘           └┘              
pid  ───┘           └┘              
st   ───────────────────────────────┘└─
 34    have h2 : 2 * i = (1 + 1) * i := rfl,
id                                  └─┘
src    └──────────┘  └┘└──┘  └──┘└─┘
typ    └──────────┘  └┘└──┘ └──┘└─┘
doc    └──────────┘    └┘ └──┘  └──┘
txt    └──────────┘    └┘ └──┘  └──┘
par    └──────────┘    └┘ └──┘  └──┘
pid    └─────┘└───┘    └┘ └──┘  └──┘
st   ─────────────────────────────────────┘└─
 35    simpa only [h2, add_mul, one_mul,
id                 └┘  └─────┘  └─────┘
src    └──────────┘  └┘└─────┘└┘└─────┘└─
typ    └──────────┘└┘└┘└─────┘└┘└─────┘└─
doc    └──────────┘  └┘       └┘       └─
txt    └──────────┘  └┘       └┘       └─
par    └──────────┘  └┘       └┘       └─
pid         └──┘└┘  └┘       └┘       └─
st   ────────────────────────────────────
 36      add_lt_add_iff_left, not_lt] using h1
id       └─────────────────┘  └────┘        └┘
src  ───┘└─────────────────┘└┘└────┘└──────┘  
typ  ───┘└─────────────────┘└┘└────┘└──────┘└┘
doc  ───┘                   └┘      └──────┘  
txt  ───┘                   └┘      └──────┘  
par  ───┘                   └┘      └──────┘  
pid  ───┘                   └┘      └────┘  
st   ─────────────────────────────────────────┘
 37  end
st   └─┘
 38  
 39  lemma mul_symdiv_eq {i j : int} :
id                              └─┘
src                             └─┘
typ                             └─┘
 40  j * (symdiv i j) = i - (symmod i j) :=
id      └────┘        └────┘  
src      └────┘           └────┘
typ     └────┘        └────┘  
 41  begin
st   └─────
 42    unfold symdiv, unfold symmod,
src    └───────────┘  └───────────┘
typ    └───────────┘  └───────────┘
doc    └───────────┘  └───────────┘
txt    └───────────┘  └───────────┘
par    └───────────┘  └───────────┘
pid          └─────┘        └─────┘
st   ──────────────┘└─────────────┘└─
 43    by_cases h1 : (2 * (i % j)) < j,
id                               
src    └───────┘  └─┘ └┘   └─┘
typ    └───────┘  └─┘ └┘  └─┘
doc    └───────┘  └─┘ └┘     └─┘ 
txt    └───────┘  └─┘ └┘     └─┘ 
par    └───────┘  └─┘ └┘     └─┘ 
pid              └─┘ └┘     └─┘ 
st   ────────────────────────────────┘└─
 44    { repeat {rw if_pos h1},
id                  └────┘ └┘
src      └──────┘└─┘└────┘  
typ      └──────┘└─┘└────┘└┘
doc      └──────┘└─┘        
txt      └──────┘└─┘        
par      └──────┘└─┘        
pid            └───┘        
st   ───┘└──────────────────┘└┘
 45      rw [int.mod_def, sub_sub_cancel] },
id           └─────────┘  └────────────┘
src      └──┘└─────────┘└┘└────────────┘└┘
typ      └──┘└─────────┘└┘└────────────┘└┘
doc      └──┘           └┘              └┘
txt      └──┘           └┘              └┘
par      └──┘           └┘              └┘
pid        └┘           └┘              
st   ──────────────────┘└──────────────┘└┘
 46    { repeat {rw if_neg h1},
id                  └────┘ └┘
src      └──────┘└─┘└────┘  
typ      └──────┘└─┘└────┘└┘
doc      └──────┘└─┘        
txt      └──────┘└─┘        
par      └──────┘└─┘        
pid            └───┘        
st   ───────────────────────┘└┘
 47      rw [int.mod_def, sub_sub, sub_sub_cancel,
id           └─────────┘  └─────┘  └────────────┘
src      └──┘└─────────┘└┘└─────┘└┘└────────────┘└─
typ      └──┘└─────────┘└┘└─────┘└┘└────────────┘└─
doc      └──┘           └┘       └┘              └─
txt      └──┘           └┘       └┘              └─
par      └──┘           └┘       └┘              └─
pid        └┘           └┘       └┘              └─
st   ──────────────────┘└───────┘└──────────────┘└─
 48        mul_add, mul_one] }
id         └─────┘  └─────┘
src  ─────┘└─────┘└┘└─────┘└┘
typ  ─────┘└─────┘└┘└─────┘└┘
doc  ─────┘       └┘       └┘
txt  ─────┘       └┘       └┘
par  ─────┘       └┘       └┘
pid  ─────┘       └┘       
st   ────────────┘└───────┘└─
 49  end
st   ──┘
 50  
 51  lemma symmod_eq {i j : int} :
id                          └─┘
src                         └─┘
typ                         └─┘
 52    symmod i j = i - j * (symdiv i j) :=
id     └────┘         └────┘  
src    └────┘             └────┘
typ    └────┘         └────┘  
 53  by rw [mul_symdiv_eq, sub_sub_cancel]
id          └───────────┘  └────────────┘
src     └──┘└───────────┘└┘└────────────┘└─
typ     └──┘└───────────┘└┘└────────────┘└─
doc     └──┘             └┘              └─
txt     └──┘             └┘              └─
par     └──┘             └┘              └─
pid       └┘             └┘              
st     └────────────────┘└──────────────┘
 54  
src  
typ  
doc  
txt  
par  
pid  
st   
 55  /- (sgm v b as n) is the new value assigned to the nth variable
src  ────────────────────────────────────────────────────────────────
typ  ────────────────────────────────────────────────────────────────
doc  ────────────────────────────────────────────────────────────────
txt  ────────────────────────────────────────────────────────────────
par  ────────────────────────────────────────────────────────────────
pid  ────────────────────────────────────────────────────────────────
st   ────────────────────────────────────────────────────────────────
 56     after a single step of equality elimination using valuation v,
src  ──────────────────────────────────────────────────────────────────
typ  ──────────────────────────────────────────────────────────────────
doc  ──────────────────────────────────────────────────────────────────
txt  ──────────────────────────────────────────────────────────────────
par  ──────────────────────────────────────────────────────────────────
pid  ──────────────────────────────────────────────────────────────────
st   ──────────────────────────────────────────────────────────────────
 57     term ⟨b, as⟩, and variable index n. If v satisfies the initial
src  ──────────────────────────────────────────────────────────────────
typ  ──────────────────────────────────────────────────────────────────
doc  ──────────────────────────────────────────────────────────────────
txt  ──────────────────────────────────────────────────────────────────
par  ──────────────────────────────────────────────────────────────────
pid  ──────────────────────────────────────────────────────────────────
st   ──────────────────────────────────────────────────────────────────
 58     constraint set, then (v ⟨n ↦ sgm v b as n⟩) satisfies the new
src  ─────────────────────────────────────────────────────────────────
typ  ─────────────────────────────────────────────────────────────────
doc  ─────────────────────────────────────────────────────────────────
txt  ─────────────────────────────────────────────────────────────────
par  ─────────────────────────────────────────────────────────────────
pid  ─────────────────────────────────────────────────────────────────
st   ─────────────────────────────────────────────────────────────────
 59     constraint set after equality elimination. -/
src  ────────────────────────────────────────────────┘
typ  ────────────────────────────────────────────────┘
doc  ────────────────────────────────────────────────┘
txt  ────────────────────────────────────────────────┘
par  ────────────────────────────────────────────────┘
pid  ────────────────────────────────────────────────┘
st   ────────────────────────────────────────────────┘
 60  def sgm (v : nat → int) (b : int) (as : list int) (n : nat) :=
id                └─┘   └─┘       └─┘        └──┘ └─┘       └─┘
src               └─┘   └─┘       └─┘        └──┘ └─┘       └─┘
typ               └─┘   └─┘       └─┘        └──┘ └─┘       └─┘
 61  let a_n : int := get n as in
id             └─┘    └─┘  └┘
src            └─┘    └─┘
typ            └─┘    └─┘  └┘
 62  let m : int := a_n + 1 in
id           └─┘    └─┘ 
src          └─┘        
typ          └─┘    └─┘ 
 63  ((symmod b m) + (coeffs.val v (as.map (λ x, symmod x m)))) / m
id     └────┘      └────────┘   └┘└──┘      └────┘        
src    └────┘        └────────┘      └──┘       └────┘         
typ    └────┘      └────────┘   └┘└──┘      └────┘        
 64  
 65  open_locale list.func
 66  
 67  def rhs : nat → int → list int → term
id             └─┘  └─┘   └──┘ └─┘   └──┘
src            └─┘   └─┘   └──┘ └─┘   └──┘
typ            └─┘  └─┘   └──┘ └─┘   └──┘
 68  | n b as :=
id       └┘
typ      └┘
 69    let m := get n as + 1 in
id             └─┘      
src             └─┘      
typ            └─┘      
 70    ⟨(symmod b m), (as.map (λ x, symmod x m)) {n ↦ -m}⟩
id       └────┘         └──┘      └────┘        
src      └────┘          └──┘       └────┘           
typ      └────┘         └──┘      └────┘        
 71  
 72  lemma rhs_correct_aux {v : nat → int} {m : int} {as : list int} :
id                              └─┘   └─┘       └─┘        └──┘ └─┘
src                             └─┘   └─┘       └─┘        └──┘ └─┘
typ                             └─┘   └─┘       └─┘        └──┘ └─┘
 73  ∀ {k}, ∃ d, (m * d +
id              
src                  
typ             
 74    coeffs.val_between v (as.map (λ (x : ℤ), symmod x m)) 0 k =
id     └────────────────┘   └┘└──┘            └────┘        
src    └────────────────┘      └──┘            └────┘           
typ    └────────────────┘   └┘└──┘            └────┘        
 75        coeffs.val_between v as 0 k)
id         └────────────────┘  └┘   
src        └────────────────┘
typ        └────────────────┘  └┘   
 76  | 0 :=
 77    begin
st     └─────
 78      existsi (0 : int),
id                    └─┘
src      └──────┘ └──┘└─┘
typ      └──────┘ └──┘└─┘
doc      └──────┘ └──┘   
txt      └──────┘ └──┘   
par      └──────┘ └──┘   
pid              └──┘   
st   ────────────────────┘└─
 79      simp only [add_zero, mul_zero, coeffs.val_between]
id                  └──────┘  └──────┘  └────────────────┘
src      └─────────┘└──────┘└┘└──────┘└┘└────────────────┘└─
typ      └─────────┘└──────┘└┘└──────┘└┘└────────────────┘└─
doc      └─────────┘        └┘        └┘                  └─
txt      └─────────┘        └┘        └┘                  └─
par      └─────────┘        └┘        └┘                  └─
pid          └──┘└┘        └┘        └┘                  
st   ───────────────────────────────────────────────────────
 80    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
 81  | (k+1) :=
id       
src      
typ      
 82    begin
st     └─────
 83      simp only [zero_add, coeffs.val_between, list.map],
id                  └──────┘  └────────────────┘  └──────┘
src      └─────────┘└──────┘└┘└────────────────┘└┘└──────┘
typ      └─────────┘└──────┘└┘└────────────────┘└┘└──────┘
doc      └─────────┘        └┘                  └┘        
txt      └─────────┘        └┘                  └┘        
par      └─────────┘        └┘                  └┘        
pid          └──┘└┘        └┘                  └┘        
st   ─────────────────────────────────────────────────────┘└─
 84      cases @rhs_correct_aux k with d h1, rw ← h1,
id              └─────────────┘                  └┘
src      └────┘                 └────────┘  └───┘
typ      └────┘ └─────────────┘└────────┘  └───┘└┘
doc      └────┘                 └────────┘  └───┘
txt      └────┘                 └────────┘  └───┘
par      └────┘                 └────────┘  └───┘
pid                            └────────┘    └─┘
st   ─────────────────────────────────────┘└───────┘└─
 85      by_cases hk : k < as.length,
id                       └───────┘
src      └───────┘  └─┘ └───────┘
typ      └───────┘  └─┘└───────┘
doc      └───────┘  └─┘  
txt      └───────┘  └─┘  
par      └───────┘  └─┘  
pid                └─┘  
st   ──────────────────────────────┘└─
 86      { rw [get_map hk, symmod_eq, sub_mul],
id             └─────┘ └┘  └───────┘  └─────┘
src        └──┘└─────┘  └┘└───────┘└┘└─────┘
typ        └──┘└─────┘└┘└┘└───────┘└┘└─────┘
doc        └──┘         └┘         └┘       
txt        └──┘         └┘         └┘       
par        └──┘         └┘         └┘       
pid          └┘         └┘         └┘       
st   ─────┘└────────────┘└─────────┘└───────┘└──
 87        existsi (d + (symdiv (get k as) m * v k)),
id                     └────┘  └─┘   └┘     
src        └──────┘   └────┘ └─┘   └┘   └┘
typ        └──────┘  └────┘ └─┘ └┘└┘└┘
doc        └──────┘                 └┘    └┘
txt        └──────┘                 └┘    └┘
par        └──────┘                 └┘    └┘
pid                                └┘    └┘
st   ──────────────────────────────────────────────┘└─
 88        ring },
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
pid            
st   ──────────┘└┘
 89      { rw not_lt at hk,
id            └────┘
src        └─┘└────┘└────┘
typ        └─┘└────┘└────┘
doc        └─┘      └────┘
txt        └─┘      └────┘
par        └─┘      └────┘
pid                └────┘
st   ────────────────────┘└─
 90        repeat {rw get_eq_default_of_le},
id                    └──────────────────┘
src        └──────┘└─┘└──────────────────┘
typ        └──────┘└─┘└──────────────────┘
doc        └──────┘└─┘                    
txt        └──────┘└─┘                    
par        └──────┘└─┘                    
pid              └───┘                    
st   ────────────────────────────────────┘└┘
 91        existsi d,
id                 
src        └──────┘
typ        └──────┘
doc        └──────┘
txt        └──────┘
par        └──────┘
pid               
st   ──────────────┘└─
 92        rw add_assoc,
id            └───────┘
src        └─┘└───────┘
typ        └─┘└───────┘
doc        └─┘
txt        └─┘
par        └─┘
pid          
st   ─────────────────┘└─
 93        exact hk,
id               └┘
src        └────┘
typ        └────┘└┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ─────────────┘└─
 94        simp only [hk, list.length_map] }
id                    └┘  └─────────────┘
src        └─────────┘  └┘└─────────────┘└┘
typ        └─────────┘└┘└┘└─────────────┘└┘
doc        └─────────┘  └┘               └┘
txt        └─────────┘  └┘               └┘
par        └─────────┘  └┘               └┘
pid            └──┘└┘  └┘               
st   ─────────────────────────────────────┘└─
 95    end
st   ────┘
 96  
 97  open_locale omega
 98  
 99  lemma rhs_correct {v : nat → int}
id                          └─┘   └─┘
src                         └─┘   └─┘
typ                         └─┘   └─┘
100    {b : int} {as : list int} (n : nat) :
id          └─┘        └──┘ └─┘       └─┘
src         └─┘        └──┘ └─┘       └─┘
typ         └─┘        └──┘ └─┘       └─┘
101    0 < get n as →
id        └─┘  └┘
src       └─┘
typ       └─┘  └┘
102    0 = term.val v (b,as) →
id        └──────┘   └┘
src       └──────┘   
typ       └──────┘   └┘
103    v n = term.val (v ⟨n ↦ sgm v b as n⟩) (rhs n b as) :=
id        └──────┘     └─┘   └┘    └─┘   └┘
src         └──────┘       └─┘            └─┘
typ       └──────┘     └─┘   └┘    └─┘   └┘
104  begin
st   └─────
105    intros h0 h1,
src    └──────────┘
typ    └──────────┘
doc    └──────────┘
txt    └──────────┘
par    └──────────┘
pid          └────┘
st   ─────────────┘└─
106    let a_n := get n as,
id                └─┘  └┘
src    └─────────┘└─┘ 
typ    └─────────┘└─┘└┘
doc    └─────────┘    
txt    └─────────┘    
par    └─────────┘    
pid    └─────┘└─┘    
st   ────────────────────┘└─
107    let m := a_n + 1,
id              └─┘ 
src    └───────┘   └┘
typ    └───────┘└─┘└┘
doc    └───────┘    └┘
txt    └───────┘    └┘
par    └───────┘    └┘
pid    └───┘└─┘    
st   ─────────────────┘└─
108    have h3 : m ≠ 0,
id                
src    └────────┘ └┘
typ    └────────┘└┘
doc    └────────┘  └┘
txt    └────────┘  └┘
par    └────────┘  └┘
pid    └─────┘└─┘  
st   ────────────────┘└─
109    { apply ne_of_gt, apply lt_trans h0, simp [a_n, m] },
id             └──────┘        └──────┘ └┘        └─┘  
src      └────┘└──────┘  └────┘└──────┘    └────┘   └┘ └┘
typ      └────┘└──────┘  └────┘└──────┘└┘  └────┘└─┘└┘└┘
doc      └────┘          └────┘            └────┘   └┘ └┘
txt      └────┘          └────┘            └────┘   └┘ └┘
par      └────┘          └────┘            └────┘   └┘ └┘
pid                                             └┘ 
st   ───┘└────────────┘└─────────────────┘└──────────────┘└┘
110    have h2 : m * (sgm v b as n) = (symmod b m) +
id                   └─┘                   
src    └────────┘  └─┘     └┘         └┘ 
typ    └────────┘  └─┘    └┘        └┘ 
doc    └────────┘           └┘          └┘ 
txt    └────────┘           └┘          └┘ 
par    └────────┘           └┘          └┘ 
pid    └─────┘└─┘           └┘          └┘ 
st   ────────────────────────────────────────────────
111      coeffs.val v (as.map (λ x, symmod x m)),
id       └────────┘   └────┘       └────┘   
src  ───┘└────────┘  └────┘  └──┘└────┘  └┘
typ  ───┘└────────┘ └────┘  └──┘└────┘ └┘
doc  ───┘                    └──┘        └┘
txt  ───┘                    └──┘        └┘
par  ───┘                    └──┘        └┘
pid  ───┘                    └──┘        └┘
st   ──────────────────────────────────────────┘└─
112    { simp only [sgm, mul_comm m],
id                  └─┘  └──────┘ 
src      └─────────┘└─┘└┘└──────┘ 
typ      └─────────┘└─┘└┘└──────┘
doc      └─────────┘   └┘         
txt      └─────────┘   └┘         
par      └─────────┘   └┘         
pid          └──┘└┘   └┘         
st   ───┘└─────────────────────────┘└─
113      rw [int.div_mul_cancel],
id           └────────────────┘
src      └──┘└────────────────┘
typ      └──┘└────────────────┘
doc      └──┘                  
txt      └──┘                  
par      └──┘                  
pid        └┘                  
st   ─────────────────────────┘└──
114      have h4 : ∃ c, m * c + (symmod b (get n as + 1) +
id                                       └─┘ 
src      └────────┘└┘             └─┘    └──┘ 
typ      └────────┘└┘             └─┘   └──┘ 
doc      └────────┘ └┘                     └──┘ 
txt      └────────┘ └┘                     └──┘ 
par      └────────┘ └┘                     └──┘ 
pid      └─────┘└─┘ └┘                     └──┘ 
st   ──────────────────────────────────────────────────────
115        coeffs.val v (as.map (λ (x : ℤ), symmod x m))) = term.val v (b,as),
id         └────────┘    └────┘             └────┘         └──────┘   └┘
src  ─────┘└────────┘  └────┘  └────┘ └─┘└────┘  └──┘ └──────┘    
typ  ─────┘└────────┘  └────┘  └────┘ └─┘└────┘ └──┘ └──────┘└┘
doc  ─────┘                    └────┘ └─┘        └──┘              
txt  ─────┘                    └────┘ └─┘        └──┘              
par  ─────┘                    └────┘ └─┘        └──┘              
pid  ─────┘                    └────┘ └─┘        └──┘              
st   ───────────────────────────────────────────────────────────────────────┘└─
116      { have h5: ∃ d,  m * d +
id                    
src        └───────┘└┘└┘    
typ        └───────┘└┘└┘    
doc        └───────┘ └┘ └┘    
txt        └───────┘ └┘ └┘    
par        └───────┘ └┘ └┘    
pid        └─────┘└┘ └┘ └┘    
st   ─────┘└──────────────────────
117          (coeffs.val v (as.map (λ x, symmod x m))) = coeffs.val v as,
id                          └────┘       └────┘         └────────┘  └┘
src  ───────┘             └────┘  └──┘└────┘  └──┘ └────────┘ 
typ  ───────┘             └────┘  └──┘└────┘ └──┘ └────────┘└┘
doc  ───────┘                     └──┘        └──┘            
txt  ───────┘                     └──┘        └──┘            
par  ───────┘                     └──┘        └──┘            
pid  ───────┘                     └──┘        └──┘            
st   ──────────────────────────────────────────────────────────────────┘└─
118        { simp only [coeffs.val, list.length_map], apply rhs_correct_aux },
id                      └────────┘  └─────────────┘         └─────────────┘
src          └─────────┘└────────┘└┘└─────────────┘  └────┘└─────────────┘
typ          └─────────┘└────────┘└┘└─────────────┘  └────┘└─────────────┘
doc          └─────────┘          └┘                 └────┘               
txt          └─────────┘          └┘                 └────┘               
par          └─────────┘          └┘                 └────┘               
pid              └──┘└┘          └┘                                     
st   ───────┘└─────────────────────────────────────┘└──────────────────────┘└┘
119        cases h5 with d h5, rw symmod_eq,
id               └┘               └───────┘
src        └────┘  └────────┘  └─┘└───────┘
typ        └────┘└┘└────────┘  └─┘└───────┘
doc        └────┘  └────────┘  └─┘
txt        └────┘  └────────┘  └─┘
par        └────┘  └────────┘  └─┘
pid               └────────┘    
st   ───────────────────────┘└────────────┘└─
120        existsi (symdiv b m + d),
id                  └────┘     
src        └──────┘ └────┘    
typ        └──────┘ └────┘ 
doc        └──────┘           
txt        └──────┘           
par        └──────┘           
pid                          
st   ─────────────────────────────┘└─
121        unfold term.val, rw ← h5,
id                               └┘
src        └─────────────┘  └───┘
typ        └─────────────┘  └───┘└┘
doc        └─────────────┘  └───┘
txt        └─────────────┘  └───┘
par        └─────────────┘  └───┘
pid              └───────┘    └─┘
st   ────────────────────┘└───────┘└─
122        simp only [term.val, mul_add, add_mul, m, a_n],
id                    └──────┘  └─────┘  └─────┘    └─┘
src        └─────────┘└──────┘└┘└─────┘└┘└─────┘└┘ └┘   
typ        └─────────┘└──────┘└┘└─────┘└┘└─────┘└┘└┘└─┘
doc        └─────────┘        └┘       └┘       └┘ └┘   
txt        └─────────┘        └┘       └┘       └┘ └┘   
par        └─────────┘        └┘       └┘       └┘ └┘   
pid            └──┘└┘        └┘       └┘       └┘ └┘   
st   ───────────────────────────────────────────────────┘└─
123        ring },
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
pid            
st   ──────────┘└┘
124      cases h4 with c h4,
id             └┘
src      └────┘  └────────┘
typ      └────┘└┘└────────┘
doc      └────┘  └────────┘
txt      └────┘  └────────┘
par      └────┘  └────────┘
pid             └────────┘
st   ─────────────────────┘└─
125      rw [dvd_add_iff_right (dvd_mul_right m c), h4, ← h1],
id           └───────────────┘  └───────────┘     └┘    └┘
src      └──┘└───────────────┘ └───────────┘  └─┘  └──┘  
typ      └──┘└───────────────┘ └───────────┘└─┘└┘└──┘└┘
doc      └──┘                                 └─┘  └──┘  
txt      └──┘                                 └─┘  └──┘  
par      └──┘                                 └─┘  └──┘  
pid        └┘                                 └─┘  └──┘  
st   ────────────────────────────────────────────┘└──┘└────┘└──
126      apply dvd_zero },
id             └──────┘
src      └────┘└──────┘
typ      └────┘└──────┘
doc      └────┘        
txt      └────┘        
par      └────┘        
pid                   
st   ──────────────────┘└┘
127    apply calc v n
src    └────┘      
typ    └────┘      
doc    └────┘      
txt    └────┘      
par    └────┘      
pid               
st   ─────────────────
128        = -(m * sgm v b as n) + (symmod b m) +
id           
src  ─────┘            └┘          └┘ 
typ  ─────┘            └┘          └┘ 
doc  ─────┘             └┘          └┘ 
txt  ─────┘             └┘          └┘ 
par  ─────┘             └┘          └┘ 
pid  ─────┘             └┘          └┘ 
st   ─────────────────────────────────────────────
129          (coeffs.val_except n v (as.map (λ x, symmod x m))) :
id            └───────────────┘      └────┘       └────┘   
src  ───────┘ └───────────────┘   └────┘  └──┘└────┘  └─────
typ  ───────┘ └───────────────┘   └────┘  └──┘└────┘ └─────
doc  ───────┘                             └──┘        └─────
txt  ───────┘                             └──┘        └─────
par  ───────┘                             └──┘        └─────
pid  ───────┘                             └──┘        └─────
st   ─────────────────────────────────────────────────────────────
130          begin
src  ───────┘     
typ  ───────┘     
doc  ───────┘     
txt  ───────┘     
par  ───────┘     
pid  ───────┘     
st   ───────┘└─────
131            rw [h2, ← coeffs.val_except_add_eq n],
id                 └┘    └──────────────────────┘ 
src  ─────────┘└──┘  └──┘└──────────────────────┘ └─
typ  ─────────┘└──┘└┘└──┘└──────────────────────┘└─
doc  ─────────┘└──┘  └──┘                         └─
txt  ─────────┘└──┘  └──┘                         └─
par  ─────────┘└──┘  └──┘                         └─
pid  ─────────────┘  └──┘                         └──
st   ───────────────┘└────────────────────────────┘└──
132            have hn : n < as.length,
id                         └───────┘
src  ─────────┘└────────┘ └───────┘└─
typ  ─────────┘└────────┘└───────┘└─
doc  ─────────┘└────────┘           └─
txt  ─────────┘└────────┘           └─
par  ─────────┘└────────┘           └─
pid  ───────────────────┘           └─
st   ────────────────────────────────┘└─
133            { by_contra hc, rw not_lt at hc,
id                                └────┘
src  ───────────┘└──────────┘└┘└─┘└────┘└────┘└─
typ  ───────────┘└──────────┘└┘└─┘└────┘└────┘└─
doc  ───────────┘└──────────┘└┘└─┘      └────┘└─
txt  ───────────┘└──────────┘└┘└─┘      └────┘└─
par  ───────────┘└──────────┘└┘└─┘      └────┘└─
pid  ────────────────────────────┘      └───────
st   ──────────┘└───────────┘└───────────────┘└─
134              rw (get_eq_default_of_le n hc) at h0,
id                   └──────────────────┘  └┘
src  ───────────┘└─┘ └──────────────────┘   └─────┘└─
typ  ───────────┘└─┘ └──────────────────┘└┘└─────┘└─
doc  ───────────┘└─┘                        └─────┘└─
txt  ───────────┘└─┘                        └─────┘└─
par  ───────────┘└─┘                        └─────┘└─
pid  ──────────────┘                        └────────
st   ───────────────────────────────────────────────┘└─
135              cases h0 },
id                     └┘
src  ───────────┘└────┘  └──
typ  ───────────┘└────┘└┘└──
doc  ───────────┘└────┘  └──
txt  ───────────┘└────┘  └──
par  ───────────┘└────┘  └──
pid  ─────────────────┘  └───
st   ────────────────────┘└─
136            rw get_map hn,
id                └─────┘ └┘
src  ─────────┘└─┘└─────┘  └─
typ  ─────────┘└─┘└─────┘└┘└─
doc  ─────────┘└─┘         └─
txt  ─────────┘└─┘         └─
par  ─────────┘└─┘         └─
pid  ────────────┘         └─
st   ──────────────────────┘└─
137            simp only [a_n, m],
id                        └─┘  
src  ─────────┘└─────────┘   └┘ └─
typ  ─────────┘└─────────┘└─┘└┘└─
doc  ─────────┘└─────────┘   └┘ └─
txt  ─────────┘└─────────┘   └┘ └─
par  ─────────┘└─────────┘   └┘ └─
pid  ────────────────────┘   └┘ └──
st   ───────────────────────────┘└─
138            rw [add_comm, symmod_add_one_self h0],
id                 └──────┘  └─────────────────┘ └┘
src  ─────────┘└──┘└──────┘└┘└─────────────────┘  └─
typ  ─────────┘└──┘└──────┘└┘└─────────────────┘└┘└─
doc  ─────────┘└──┘        └┘                     └─
txt  ─────────┘└──┘        └┘                     └─
par  ─────────┘└──┘        └┘                     └─
pid  ─────────────┘        └┘                     └──
st   ─────────────────────┘└──────────────────────┘└──
139            ring
src  ─────────┘└────
typ  ─────────┘└────
doc  ─────────┘└────
txt  ─────────┘└────
par  ─────────┘└────
pid  ───────────────
st   ───────────────
140          end
src  ───────┘└───
typ  ───────┘└───
doc  ───────┘└───
txt  ───────┘└───
par  ───────┘└───
pid  ────────────
st   ───────┘└─┘
141    ... = term.val (v⟨n↦sgm v b as n⟩) (rhs n b as) :
id           └──────┘     └─┘             └─┘   └┘
src  ─────┘ └──────┘     └─┘      └┘ └─┘    └───
typ  ─────┘ └──────┘    └─┘      └┘ └─┘└┘└───
doc  ─────┘                       └┘        └───
txt  ─────┘                       └┘        └───
par  ─────┘                       └┘        └───
pid  ─────┘                       └┘        └───
st   ────────────────────────────────────────────────────
142          begin
src  ───────┘     
typ  ───────┘     
doc  ───────┘     
txt  ───────┘     
par  ───────┘     
pid  ───────┘     
st   ───────┘└─────
143            unfold rhs, unfold term.val,
src  ─────────┘└────────┘└┘└─────────────┘└─
typ  ─────────┘└────────┘└┘└─────────────┘└─
doc  ─────────┘└────────┘└┘└─────────────┘└─
txt  ─────────┘└────────┘└┘└─────────────┘└─
par  ─────────┘└────────┘└┘└─────────────┘└─
pid  ───────────────────────────────────────
st   ───────────────────┘└───────────────┘└─
144            rw [← coeffs.val_except_add_eq n, get_set, update_eq],
id                   └──────────────────────┘   └─────┘  └───────┘
src  ─────────┘└────┘└──────────────────────┘ └┘└─────┘└┘└───────┘└─
typ  ─────────┘└────┘└──────────────────────┘└┘└─────┘└┘└───────┘└─
doc  ─────────┘└────┘                         └┘       └┘         └─
txt  ─────────┘└────┘                         └┘       └┘         └─
par  ─────────┘└────┘                         └┘       └┘         └─
pid  ───────────────┘                         └┘       └┘         └──
st   ─────────────────────────────────────────┘└───────┘└─────────┘└──
145            have h2 : ∀ a b c : int, a + b + c = b + (c + a) := by {intros, ring},
id                                 └─┘
src  ─────────┘└────────┘ └───────┘└─┘             └───┘  └┘└────┘└┘└──┘└─
typ  ─────────┘└────────┘ └───────┘└─┘             └───┘  └┘└────┘└┘└──┘└─
doc  ─────────┘└────────┘ └───────┘                └───┘  └┘└────┘└┘└──┘└─
txt  ─────────┘└────────┘ └───────┘                └───┘  └┘└────┘└┘└──┘└─
par  ─────────┘└────────┘ └───────┘                └───┘  └┘└────┘└┘└──┘└─
pid  ───────────────────┘ └───────┘                └───┘  └────────────────
st   ───────────────────────────────────────────────────────────────┘└──────┘└────┘└─
146            rw (h2 (- _)),
id                 └┘
src  ─────────┘└─┘     └──┘└─
typ  ─────────┘└─┘ └┘  └──┘└─
doc  ─────────┘└─┘     └──┘└─
txt  ─────────┘└─┘     └──┘└─
par  ─────────┘└─┘     └──┘└─
pid  ────────────┘     └─────
st   ──────────────────────┘└─
147            apply fun_mono_2 rfl,
id                   └────────┘ └─┘
src  ───────────────┘└────────┘└─┘└─
typ  ───────────────┘└────────┘└─┘└─
doc  ───────────────┘             └─
txt  ───────────────┘             └─
par  ───────────────┘             └─
pid  ───────────────┘             └─
st   ─────────────────────────────┘└─
148            apply fun_mono_2,
id                   └────────┘
src  ───────────────┘└────────┘└─
typ  ───────────────┘└────────┘└─
doc  ───────────────┘          └─
txt  ───────────────┘          └─
par  ───────────────┘          └─
pid  ───────────────┘          └─
st   ─────────────────────────┘└─
149            { rw coeffs.val_except_update_set },
id                  └──────────────────────────┘
src  ───────────┘└─┘└──────────────────────────┘└──
typ  ───────────┘└─┘└──────────────────────────┘└──
doc  ───────────┘└─┘                            └──
txt  ───────────┘└─┘                            └──
par  ───────────┘└─┘                            └──
pid  ──────────────┘                            └───
st   ──────────┘└───────────────────────────────┘└─
150            { simp only [m, a_n], ring }
id                            └─┘
src  ───────────┘└─────────┘ └┘   └┘└───┘└─
typ  ───────────┘└─────────┘└┘└─┘└┘└───┘└─
doc  ───────────┘└─────────┘ └┘   └┘└───┘└─
txt  ───────────┘└─────────┘ └┘   └┘└───┘└─
par  ───────────┘└─────────┘ └┘   └┘└───┘└─
pid  ──────────────────────┘ └┘   └─────────
st   ─────────────────────────────┘└─────┘└─
151          end
src  ───────────┘
typ  ───────────┘
doc  ───────────┘
txt  ───────────┘
par  ───────────┘
pid  ──────────┘
st   ──────────┘
152  end
st   └─┘
153  
154  def sym_sym (m b : int) : int :=
id                      └─┘    └─┘
src                     └─┘    └─┘
typ                     └─┘    └─┘
155  symdiv b m + symmod b m
id   └────┘    └────┘  
src  └────┘      └────┘
typ  └────┘    └────┘  
156  
157  def coeffs_reduce : nat → int → list int → term
id                       └─┘  └─┘   └──┘ └─┘   └──┘
src                      └─┘   └─┘   └──┘ └─┘   └──┘
typ                      └─┘  └─┘   └──┘ └─┘   └──┘
158  | n b as :=
id       └┘
typ      └┘
159    let a := get n as in
id             └─┘
src             └─┘
typ            └─┘
160    let m := a + 1 in
id              
src               
typ             
161    (sym_sym m b, (as.map (sym_sym m)) {n ↦ -a})
id     └─────┘        └──┘  └─────┘       
src    └─────┘         └──┘  └─────┘         
typ    └─────┘        └──┘  └─────┘       
162  
163  lemma coeffs_reduce_correct
164    {v : nat → int} {b : int} {as : list int} {n : nat} :
id          └─┘   └─┘       └─┘        └──┘ └─┘       └─┘
src         └─┘   └─┘       └─┘        └──┘ └─┘       └─┘
typ         └─┘   └─┘       └─┘        └──┘ └─┘       └─┘
165    0 < get n as →
id        └─┘  └┘
src       └─┘
typ       └─┘  └┘
166    0 = term.val v (b,as) →
id        └──────┘   └┘
src       └──────┘   
typ       └──────┘   └┘
167    0 = term.val (v ⟨n ↦ sgm v b as n⟩) (coeffs_reduce n b as) :=
id        └──────┘     └─┘   └┘    └───────────┘   └┘
src       └──────┘       └─┘            └───────────┘
typ       └──────┘     └─┘   └┘    └───────────┘   └┘
168  begin
st   └─────
169    intros h1 h2,
src    └──────────┘
typ    └──────────┘
doc    └──────────┘
txt    └──────────┘
par    └──────────┘
pid          └────┘
st   ─────────────┘└─
170    let a_n := get n as,
id                └─┘  └┘
src    └─────────┘└─┘ 
typ    └─────────┘└─┘└┘
doc    └─────────┘    
txt    └─────────┘    
par    └─────────┘    
pid    └─────┘└─┘    
st   ────────────────────┘└─
171    let m := a_n + 1,
id              └─┘ 
src    └───────┘   └┘
typ    └───────┘└─┘└┘
doc    └───────┘    └┘
txt    └───────┘    └┘
par    └───────┘    └┘
pid    └───┘└─┘    
st   ─────────────────┘└─
172    have h3 : m ≠ 0,
id                
src    └────────┘ └┘
typ    └────────┘└┘
doc    └────────┘  └┘
txt    └────────┘  └┘
par    └────────┘  └┘
pid    └─────┘└─┘  
st   ────────────────┘└─
173    { apply ne_of_gt,
id             └──────┘
src      └────┘└──────┘
typ      └────┘└──────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───┘└────────────┘└─
174      apply lt_trans h1,
id             └──────┘ └┘
src      └────┘└──────┘
typ      └────┘└──────┘└┘
doc      └────┘        
txt      └────┘        
par      └────┘        
pid                   
st   ────────────────────┘└─
175      simp only [m, lt_add_iff_pos_right] },
id                    └──────────────────┘
src      └─────────┘ └┘└──────────────────┘└┘
typ      └─────────┘└┘└──────────────────┘└┘
doc      └─────────┘ └┘                    └┘
txt      └─────────┘ └┘                    └┘
par      └─────────┘ └┘                    └┘
pid          └──┘└┘ └┘                    
st   ───────────────────────────────────────┘└┘
176    have h4 : 0 = (term.val (v⟨n↦sgm v b as n⟩) (coeffs_reduce n b as)) * m :=
id                   └──────┘     └─┘             └───────────┘   └┘    
src    └──────────┘ └──────┘     └─┘      └┘ └───────────┘    └─┘ └───
typ    └──────────┘ └──────┘    └─┘      └┘ └───────────┘└┘└─┘└───
doc    └──────────┘                        └┘                  └─┘  └───
txt    └──────────┘                        └┘                  └─┘  └───
par    └──────────┘                        └┘                  └─┘  └───
pid    └─────┘└───┘                        └┘                  └─┘  └───
st   ─────────────────────────────────────────────────────────────────────────────
177    calc  0
src  ─┘    └───
typ  ─┘    └───
doc  ─┘    └───
txt  ─┘    └───
par  ─┘    └───
pid  ─┘    └───
st   ──────────
178        = term.val v (b,as) : h2
id           └──────┘   └┘    └┘
src  ─────┘ └──────┘    └──┘  
typ  ─────┘ └──────┘└┘└──┘└┘
doc  ─────┘              └──┘  
txt  ─────┘              └──┘  
par  ─────┘              └──┘  
pid  ─────┘              └──┘  
st   ───────────────────────────────
179    ... = b + coeffs.val_except n v as
id               └───────────────┘
src  ─────┘   └───────────────┘    
typ  ─────┘   └───────────────┘    
doc  ─────┘                        
txt  ─────┘                        
par  ─────┘                        
pid  ─────┘                        
st   ─────────────────────────────────────
180            + a_n * ((rhs n b as).val (v⟨n ↦ sgm v b as n⟩)) :
id               └─┘     └─┘                    └─┘        
src  ─────────┘       └─┘    └────┘     └─┘      └────
typ  ─────────┘ └─┘   └─┘    └────┘     └─┘     └────
doc  ─────────┘              └────┘              └────
txt  ─────────┘              └────┘              └────
par  ─────────┘              └────┘              └────
pid  ─────────┘              └────┘              └────
st   ─────────────────────────────────────────────────────────────
181          begin
src  ───────┘     
typ  ───────┘     
doc  ───────┘     
txt  ───────┘     
par  ───────┘     
pid  ───────┘     
st   ───────┘└─────
182            unfold term.val,
src  ─────────┘└─────────────┘└─
typ  ─────────┘└─────────────┘└─
doc  ─────────┘└─────────────┘└─
txt  ─────────┘└─────────────┘└─
par  ─────────┘└─────────────┘└─
pid  ───────────────────────────
st   ────────────────────────┘└─
183            rw [← coeffs.val_except_add_eq n, rhs_correct n h1 h2],
id                   └──────────────────────┘   └─────────┘  └┘ └┘
src  ─────────┘└────┘└──────────────────────┘ └┘└─────────┘     └─
typ  ─────────┘└────┘└──────────────────────┘└┘└─────────┘└┘└┘└─
doc  ─────────┘└────┘                         └┘                └─
txt  ─────────┘└────┘                         └┘                └─
par  ─────────┘└────┘                         └┘                └─
pid  ───────────────┘                         └┘                └──
st   ─────────────────────────────────────────┘└───────────────────┘└──
184            simp only [a_n, add_assoc],
id                        └─┘  └───────┘
src  ─────────┘└─────────┘   └┘└───────┘└─
typ  ─────────┘└─────────┘└─┘└┘└───────┘└─
doc  ─────────┘└─────────┘   └┘         └─
txt  ─────────┘└─────────┘   └┘         └─
par  ─────────┘└─────────┘   └┘         └─
pid  ────────────────────┘   └┘         └──
st   ───────────────────────────────────┘└─
185          end
src  ────────────
typ  ────────────
doc  ────────────
txt  ────────────
par  ────────────
pid  ────────────
st   ──────────┘
186    ... = -(m * a_n * sgm v b as n) + (b + a_n * (symmod b m)) +
src  ─────┘                 └┘                 └─┘ 
typ  ─────┘                 └┘                 └─┘ 
doc  ─────┘                 └┘                 └─┘ 
txt  ─────┘                 └┘                 └─┘ 
par  ─────┘                 └┘                 └─┘ 
pid  ─────┘                 └┘                 └─┘ 
st   ───────────────────────────────────────────────────────────────
187          (coeffs.val_except n v as +
src  ───────┘                       
typ  ───────┘                       
doc  ───────┘                       
txt  ───────┘                       
par  ───────┘                       
pid  ───────┘                       
st   ────────────────────────────────────
188          a_n * coeffs.val_except n v (as.map (λ x, symmod x m))) :
id                                        └────┘       └────┘   
src  ───────┘                        └────┘  └──┘└────┘  └─────
typ  ───────┘                        └────┘  └──┘└────┘ └─────
doc  ───────┘                                └──┘        └─────
txt  ───────┘                                └──┘        └─────
par  ───────┘                                └──┘        └─────
pid  ───────┘                                └──┘        └─────
st   ──────────────────────────────────────────────────────────────────
189            begin
src  ─────────┘     
typ  ─────────┘     
doc  ─────────┘     
txt  ─────────┘     
par  ─────────┘     
pid  ─────────┘     
st   ─────────┘└─────
190              simp only [term.val, rhs, mul_add, m, a_n,
id                          └──────┘  └─┘  └─────┘    └─┘
src  ───────────┘└─────────┘└──────┘└┘└─┘└┘└─────┘└┘ └┘   └─
typ  ───────────┘└─────────┘└──────┘└┘└─┘└┘└─────┘└┘└┘└─┘└─
doc  ───────────┘└─────────┘        └┘   └┘       └┘ └┘   └─
txt  ───────────┘└─────────┘        └┘   └┘       └┘ └┘   └─
par  ───────────┘└─────────┘        └┘   └┘       └┘ └┘   └─
pid  ──────────────────────┘        └┘   └┘       └┘ └┘   └─
st   ───────────────────────────────────────────────────────
191                add_assoc, add_left_inj, add_comm, add_left_comm],
id                 └───────┘  └──────────┘  └──────┘  └───────────┘
src  ─────────────┘└───────┘└┘└──────────┘└┘└──────┘└┘└───────────┘└─
typ  ─────────────┘└───────┘└┘└──────────┘└┘└──────┘└┘└───────────┘└─
doc  ─────────────┘         └┘            └┘        └┘             └─
txt  ─────────────┘         └┘            └┘        └┘             └─
par  ─────────────┘         └┘            └┘        └┘             └─
pid  ─────────────┘         └┘            └┘        └┘             └──
st   ──────────────────────────────────────────────────────────────┘└─
192              rw [← coeffs.val_except_add_eq n,
id                     └──────────────────────┘ 
src  ───────────┘└────┘└──────────────────────┘ └─
typ  ───────────┘└────┘└──────────────────────┘└─
doc  ───────────┘└────┘                         └─
txt  ───────────┘└────┘                         └─
par  ───────────┘└────┘                         └─
pid  ─────────────────┘                         └─
st   ───────────────────────────────────────────┘└─
193                get_set, update_eq, mul_add],
id                 └─────┘  └───────┘  └─────┘
src  ─────────────┘└─────┘└┘└───────┘└┘└─────┘└─
typ  ─────────────┘└─────┘└┘└───────┘└┘└─────┘└─
doc  ─────────────┘       └┘         └┘       └─
txt  ─────────────┘       └┘         └┘       └─
par  ─────────────┘       └┘         └┘       └─
pid  ─────────────┘       └┘         └┘       └──
st   ────────────────────┘└─────────┘└───────┘└──
194              apply fun_mono_2,
id                     └────────┘
src  ───────────┘└────┘└────────┘└─
typ  ───────────┘└────┘└────────┘└─
doc  ───────────┘└────┘          └─
txt  ───────────┘└────┘          └─
par  ───────────┘└────┘          └─
pid  ─────────────────┘          └─
st   ───────────────────────────┘└─
195              { rw coeffs.val_except_eq_val_except
id                    └─────────────────────────────┘
src  ─────────────┘└─┘└─────────────────────────────┘
typ  ─────────────┘└─┘└─────────────────────────────┘
doc  ─────────────┘└─┘                               
txt  ─────────────┘└─┘                               
par  ─────────────┘└─┘                               
pid  ────────────────┘                               
st   ────────────┘└───────────────────────────────────
196                update_eq_of_ne (get_set_eq_of_ne _) },
id                 └─────────────┘  └──────────────┘
src  ─────────────┘└─────────────┘ └──────────────┘└──┘└──
typ  ─────────────┘└─────────────┘ └──────────────┘└──┘└──
doc  ─────────────┘                                └──┘└──
txt  ─────────────┘                                └──┘└──
par  ─────────────┘                                └──┘└──
pid  ─────────────┘                                └──────
st   ──────────────────────────────────────────────────┘└─
197              simp only [m], ring,
id                          
src  ───────────┘└─────────┘ └┘└──┘└─
typ  ───────────┘└─────────┘└┘└──┘└─
doc  ───────────┘└─────────┘ └┘└──┘└─
txt  ───────────┘└─────────┘ └┘└──┘└─
par  ───────────┘└─────────┘ └┘└──┘└─
pid  ──────────────────────┘ └────────
st   ────────────────────────┘└────┘└─
198            end
src  ──────────────
typ  ──────────────
doc  ──────────────
txt  ──────────────
par  ──────────────
pid  ──────────────
st   ────────────┘
199    ... = -(m * a_n * sgm v b as n) + (b + a_n * (symmod b m))
src  ─────┘                 └┘                 └──
typ  ─────┘                 └┘                 └──
doc  ─────┘                 └┘                 └──
txt  ─────┘                 └┘                 └──
par  ─────┘                 └┘                 └──
pid  ─────┘                 └┘                 └──
st   ─────────────────────────────────────────────────────────────
200          + coeffs.val_except n v (as.map (λ a_i, a_i + a_n * (symmod a_i m))) :
src  ───────┘                             └────┘                   └─────
typ  ───────┘                             └────┘                   └─────
doc  ───────┘                             └────┘                   └─────
txt  ───────┘                             └────┘                   └─────
par  ───────┘                             └────┘                   └─────
pid  ───────┘                             └────┘                   └─────
st   ───────────────────────────────────────────────────────────────────────────────
201          begin
src  ───────┘     
typ  ───────┘     
doc  ───────┘     
txt  ───────┘     
par  ───────┘     
pid  ───────┘     
st   ───────┘└─────
202            apply fun_mono_2 rfl,
id                   └────────┘ └─┘
src  ─────────┘└────┘└────────┘└─┘└─
typ  ─────────┘└────┘└────────┘└─┘└─
doc  ─────────┘└────┘             └─
txt  ─────────┘└────┘             └─
par  ─────────┘└────┘             └─
pid  ───────────────┘             └─
st   ─────────────────────────────┘└─
203            simp only [coeffs.val_except, mul_add],
id                        └───────────────┘  └─────┘
src  ─────────┘└─────────┘└───────────────┘└┘└─────┘└─
typ  ─────────┘└─────────┘└───────────────┘└┘└─────┘└─
doc  ─────────┘└─────────┘                 └┘       └─
txt  ─────────┘└─────────┘                 └┘       └─
par  ─────────┘└─────────┘                 └┘       └─
pid  ────────────────────┘                 └┘       └──
st   ───────────────────────────────────────────────┘└─
204            repeat {rw ← coeffs.val_between_map_mul},
id                          └────────────────────────┘
src  ─────────┘└──────┘└───┘└────────────────────────┘└─
typ  ─────────┘└──────┘└───┘└────────────────────────┘└─
doc  ─────────┘└──────┘└───┘                          └─
txt  ─────────┘└──────┘└───┘                          └─
par  ─────────┘└──────┘└───┘                          └─
pid  ──────────────────────┘                          └──
st   ────────────────────────────────────────────────┘└─
205            have h4 : ∀ {a b c d : int},
id                                    └─┘
src  ───────────────────┘ └──────────┘└─┘ 
typ  ───────────────────┘ └──────────┘└─┘ 
doc  ───────────────────┘ └──────────┘    
txt  ───────────────────┘ └──────────┘    
par  ───────────────────┘ └──────────┘    
pid  ───────────────────┘ └──────────┘    
st   ───────────────────────────────────────
206              a + b + (c + d) = (a + c) + (b + d),
src  ───────────┘        └┘     └┘     └──
typ  ───────────┘        └┘     └┘     └──
doc  ───────────┘        └┘     └┘     └──
txt  ───────────┘        └┘     └┘     └──
par  ───────────┘        └┘     └┘     └──
pid  ───────────┘        └┘     └┘     └──
st   ──────────────────────────────────────────────┘└─
207            { intros, ring }, rw h4,
src  ───────────┘└────┘└┘└───┘└─┘└─┘  └─
typ  ───────────┘└────┘└┘└───┘└─┘└─┘└┘└─
doc  ───────────┘└────┘└┘└───┘└─┘└─┘  └─
txt  ───────────┘└────┘└┘└───┘└─┘└─┘  └─
par  ───────────┘└────┘└┘└───┘└─┘└─┘  └─
pid  ──────────────────────────────┘  └─
st   ──────────┘└─────┘└─────┘└─────┘└─
208            have h5 : add as (list.map (has_mul.mul a_n)
id                       └─┘               └─────────┘
src  ───────────────────┘└─┘            └─────────┘   └─
typ  ───────────────────┘└─┘            └─────────┘   └─
doc  ───────────────────┘                             └─
txt  ───────────────────┘                             └─
par  ───────────────────┘                             └─
pid  ───────────────────┘                             └─
st   ───────────────────────────────────────────────────────
209              (list.map (λ (x : ℤ), symmod x (get n as + 1)) as)) =
id                                               └─┘ 
src  ───────────┘           └────┘ └─┘        └─┘    └───┘  └─┘ 
typ  ───────────┘           └────┘ └─┘        └─┘   └───┘  └─┘ 
doc  ───────────┘           └────┘ └─┘               └───┘  └─┘ 
txt  ───────────┘           └────┘ └─┘               └───┘  └─┘ 
par  ───────────┘           └────┘ └─┘               └───┘  └─┘ 
pid  ───────────┘           └────┘ └─┘               └───┘  └─┘ 
st   ──────────────────────────────────────────────────────────────────
210              list.map (λ (a_i : ℤ), a_i + a_n * symmod a_i m) as,
id               └──────┘                     └─┘   └────┘       └┘
src  ───────────┘└──────┘  └──────┘ └─┘        └────┘    └┘  └─
typ  ───────────┘└──────┘  └──────┘ └─┘    └─┘ └────┘   └┘└┘└─
doc  ───────────┘          └──────┘ └─┘                  └┘  └─
txt  ───────────┘          └──────┘ └─┘                  └┘  └─
par  ───────────┘          └──────┘ └─┘                  └┘  └─
pid  ───────────┘          └──────┘ └─┘                  └┘  └─
st   ──────────────────────────────────────────────────────────────┘└─
211            { rw [list.map_map, ←map_add_map],
id                   └──────────┘   └─────────┘
src  ───────────┘└──┘└──────────┘└─┘└─────────┘└─
typ  ───────────┘└──┘└──────────┘└─┘└─────────┘└─
doc  ───────────┘└──┘            └─┘           └─
txt  ───────────┘└──┘            └─┘           └─
par  ───────────┘└──┘            └─┘           └─
pid  ───────────────┘            └─┘           └──
st   ──────────┘└───────────────┘└────────────┘└──
212              apply fun_mono_2,
id                     └────────┘
src  ───────────┘└────┘└────────┘└─
typ  ───────────┘└────┘└────────┘└─
doc  ───────────┘└────┘          └─
txt  ───────────┘└────┘          └─
par  ───────────┘└────┘          └─
pid  ─────────────────┘          └─
st   ───────────────────────────┘└─
213              { have h5 : (λ x : int, x) = id,
id                                  └─┘       └┘
src  ───────────────────────┘  └───┘└─┘└┘ └┘ └┘└─
typ  ───────────────────────┘  └───┘└─┘└┘ └┘ └┘└─
doc  ───────────────────────┘  └───┘   └┘ └┘   └─
txt  ───────────────────────┘  └───┘   └┘ └┘   └─
par  ───────────────────────┘  └───┘   └┘ └┘   └─
pid  ───────────────────────┘  └───┘   └┘ └┘   └─
st   ────────────┘└────────────────────────────┘└─
214                { rw function.funext_iff, intro x, refl },
id                      └─────────────────┘
src  ───────────────┘└─┘└─────────────────┘└┘└─────┘└┘└───┘└──
typ  ───────────────┘└─┘└─────────────────┘└┘└─────┘└┘└───┘└──
doc  ───────────────┘└─┘                   └┘└─────┘└┘└───┘└──
txt  ───────────────┘└─┘                   └┘└─────┘└┘└───┘└──
par  ───────────────┘└─┘                   └┘└─────┘└┘└───┘└──
pid  ──────────────────┘                   └──────────────────
st   ──────────────┘└─────────────────────┘└───────┘└─────┘└─
215                rw [h5, list.map_id] },
id                     └┘  └─────────┘
src  ─────────────┘└──┘  └┘└─────────┘└┘└──
typ  ─────────────┘└──┘└┘└┘└─────────┘└┘└──
doc  ─────────────┘└──┘  └┘           └┘└──
txt  ─────────────┘└──┘  └┘           └┘└──
par  ─────────────┘└──┘  └┘           └┘└──
pid  ─────────────────┘  └┘           └────
st   ───────────────────┘└───────────┘└─
216              { apply fun_mono_2 _ rfl,
id                       └────────┘   └─┘
src  ─────────────┘└────┘└────────┘└─┘└─┘└─
typ  ─────────────┘└────┘└────────┘└─┘└─┘└─
doc  ─────────────┘└────┘          └─┘   └─
txt  ─────────────┘└────┘          └─┘   └─
par  ─────────────┘└────┘          └─┘   └─
pid  ───────────────────┘          └─┘   └─
st   ───────────────────────────────────┘└─
217                rw function.funext_iff, intro x,
id                    └─────────────────┘
src  ─────────────┘└─┘└─────────────────┘└┘└─────┘└─
typ  ─────────────┘└─┘└─────────────────┘└┘└─────┘└─
doc  ─────────────┘└─┘                   └┘└─────┘└─
txt  ─────────────┘└─┘                   └┘└─────┘└─
par  ─────────────┘└─┘                   └┘└─────┘└─
pid  ────────────────┘                   └──────────
st   ───────────────────────────────────┘└───────┘└─
218                simp only [m] } },
id                            
src  ─────────────┘└─────────┘ └┘└────
typ  ─────────────┘└─────────┘└┘└────
doc  ─────────────┘└─────────┘ └┘└────
txt  ─────────────┘└─────────┘ └┘└────
par  ─────────────┘└─────────┘ └┘└────
pid  ────────────────────────┘ └──────
st   ───────────────────────────┘└─┘└─
219            simp only [list.length_map],
id                        └─────────────┘
src  ─────────┘└─────────┘└─────────────┘└─
typ  ─────────┘└─────────┘└─────────────┘└─
doc  ─────────┘└─────────┘               └─
txt  ─────────┘└─────────┘               └─
par  ─────────┘└─────────┘               └─
pid  ────────────────────┘               └──
st   ────────────────────────────────────┘└─
220            repeat { rw [← coeffs.val_between_add, h5] },
id                            └────────────────────┘  └┘
src  ─────────┘└───────┘└────┘└────────────────────┘└┘  └┘└─
typ  ─────────┘└───────┘└────┘└────────────────────┘└┘└┘└┘└─
doc  ─────────┘└───────┘└────┘                      └┘  └┘└─
txt  ─────────┘└───────┘└────┘                      └┘  └┘└─
par  ─────────┘└───────┘└────┘                      └┘  └┘└─
pid  ────────────────────────┘                      └┘  └────
st   ──────────────────────────────────────────────┘└──┘└─
221          end
src  ────────────
typ  ────────────
doc  ────────────
txt  ────────────
par  ────────────
pid  ────────────
st   ──────────┘
222    ... = -(m * a_n * sgm v b as n) + (m * sym_sym m b)
src  ─────┘                 └┘             └─
typ  ─────┘                 └┘             └─
doc  ─────┘                 └┘             └─
txt  ─────┘                 └┘             └─
par  ─────┘                 └┘             └─
pid  ─────┘                 └┘             └─
st   ──────────────────────────────────────────────────────
223          + coeffs.val_except n v (as.map (λ a_i, m * sym_sym m a_i)) :
id                                                       └─────┘
src  ───────┘                             └────┘  └─────┘    └────
typ  ───────┘                             └────┘  └─────┘    └────
doc  ───────┘                             └────┘             └────
txt  ───────┘                             └────┘             └────
par  ───────┘                             └────┘             └────
pid  ───────┘                             └────┘             └────
st   ──────────────────────────────────────────────────────────────────────
224          begin
src  ───────┘     
typ  ───────┘     
doc  ───────┘     
txt  ───────┘     
par  ───────┘     
pid  ───────┘     
st   ───────┘└─────
225            repeat {rw add_assoc}, apply fun_mono_2, refl,
id                        └───────┘         └────────┘
src  ─────────┘└──────┘└─┘└───────┘└┘└────┘└────────┘└┘└──┘└─
typ  ─────────┘└──────┘└─┘└───────┘└┘└────┘└────────┘└┘└──┘└─
doc  ─────────┘└──────┘└─┘         └┘└────┘          └┘└──┘└─
txt  ─────────┘└──────┘└─┘         └┘└────┘          └┘└──┘└─
par  ─────────┘└──────┘└─┘         └┘└────┘          └┘└──┘└─
pid  ────────────────────┘         └───────┘          └───────
st   ─────────────────────────────┘└────────────────┘└────┘└─
226            rw ← add_assoc,
id                  └───────┘
src  ─────────┘└───┘└───────┘└─
typ  ─────────┘└───┘└───────┘└─
doc  ─────────┘└───┘         └─
txt  ─────────┘└───┘         └─
par  ─────────┘└───┘         └─
pid  ──────────────┘         └─
st   ───────────────────────┘└─
227            have h4 : ∀ (x : ℤ), x + a_n * symmod x m = m * sym_sym m x,
id                                      └─┘   └────┘           └─────┘ 
src  ───────────────────┘ └────┘        └────┘     └─────┘  └─
typ  ───────────────────┘ └────┘    └─┘ └────┘     └─────┘ └─
doc  ───────────────────┘ └────┘                            └─
txt  ───────────────────┘ └────┘                            └─
par  ───────────────────┘ └────┘                            └─
pid  ───────────────────┘ └────┘                            └─
st   ────────────────────────────────────────────────────────────────────┘└─
228            { intro x, have h5 : a_n = m - 1,
id                                  └─┘    
src  ───────────┘└─────┘└──────────┘     └───
typ  ───────────┘└─────┘└──────────┘└─┘ └───
doc  ───────────┘└─────┘└──────────┘      └───
txt  ───────────┘└─────┘└──────────┘      └───
par  ───────────┘└─────┘└──────────┘      └───
pid  ──────────────────────────────┘      └───
st   ──────────┘└──────┘└─────────────────────┘└─
229              { simp only [m],
id                            
src  ─────────────┘└─────────┘ └─
typ  ─────────────┘└─────────┘└─
doc  ─────────────┘└─────────┘ └─
txt  ─────────────┘└─────────┘ └─
par  ─────────────┘└─────────┘ └─
pid  ────────────────────────┘ └──
st   ────────────┘└────────────┘└─
230                rw add_sub_cancel },
id                    └────────────┘
src  ─────────────┘└─┘└────────────┘└──
typ  ─────────────┘└─┘└────────────┘└──
doc  ─────────────┘└─┘              └──
txt  ─────────────┘└─┘              └──
par  ─────────────┘└─┘              └──
pid  ────────────────┘              └───
st   ───────────────────────────────┘└─
231              rw [h5, sub_mul, one_mul, add_sub,
id                   └┘  └─────┘  └─────┘  └─────┘
src  ───────────┘└──┘  └┘└─────┘└┘└─────┘└┘└─────┘└─
typ  ───────────┘└──┘└┘└┘└─────┘└┘└─────┘└┘└─────┘└─
doc  ───────────┘└──┘  └┘       └┘       └┘       └─
txt  ───────────┘└──┘  └┘       └┘       └┘       └─
par  ───────────┘└──┘  └┘       └┘       └┘       └─
pid  ───────────────┘  └┘       └┘       └┘       └─
st   ─────────────────┘└───────┘└───────┘└───────┘└─
232                add_comm, add_sub_assoc, ← mul_symdiv_eq],
id                 └──────┘  └───────────┘    └───────────┘
src  ─────────────┘└──────┘└┘└───────────┘└──┘└───────────┘└─
typ  ─────────────┘└──────┘└┘└───────────┘└──┘└───────────┘└─
doc  ─────────────┘        └┘             └──┘             └─
txt  ─────────────┘        └┘             └──┘             └─
par  ─────────────┘        └┘             └──┘             └─
pid  ─────────────┘        └┘             └──┘             └──
st   ─────────────────────┘└─────────────┘└───────────────┘└──
233              simp only [sym_sym, mul_add, add_comm] },
id                          └─────┘  └─────┘  └──────┘
src  ───────────┘└─────────┘└─────┘└┘└─────┘└┘└──────┘└┘└──
typ  ───────────┘└─────────┘└─────┘└┘└─────┘└┘└──────┘└┘└──
doc  ───────────┘└─────────┘       └┘       └┘        └┘└──
txt  ───────────┘└─────────┘       └┘       └┘        └┘└──
par  ───────────┘└─────────┘       └┘       └┘        └┘└──
pid  ──────────────────────┘       └┘       └┘        └────
st   ──────────────────────────────────────────────────┘└─
234            apply fun_mono_2 (h4 _),
id                   └────────┘  └┘
src  ─────────┘└────┘└────────┘   └─┘└─
typ  ─────────┘└────┘└────────┘ └┘└─┘└─
doc  ─────────┘└────┘             └─┘└─
txt  ─────────┘└────┘             └─┘└─
par  ─────────┘└────┘             └─┘└─
pid  ───────────────┘             └────
st   ────────────────────────────────┘└─
235            apply coeffs.val_except_eq_val_except; intros x h5, refl,
id                   └─────────────────────────────┘
src  ─────────┘└────┘└─────────────────────────────┘└┘└─────────┘└┘└──┘└─
typ  ─────────┘└────┘└─────────────────────────────┘└┘└─────────┘└┘└──┘└─
doc  ─────────┘└────┘                               └┘└─────────┘└┘└──┘└─
txt  ─────────┘└────┘                               └┘└─────────┘└┘└──┘└─
par  ─────────┘└────┘                               └┘└─────────┘└┘└──┘└─
pid  ───────────────┘                               └────────────────────
st   ───────────────────────────────────────────────────────────┘└────┘└─
236            apply congr_arg,
id                   └───────┘
src  ─────────┘└────┘└───────┘└─
typ  ─────────┘└────┘└───────┘└─
doc  ─────────┘└────┘         └─
txt  ─────────┘└────┘         └─
par  ─────────┘└────┘         └─
pid  ───────────────┘         └─
st   ────────────────────────┘└─
237            apply fun_mono_2 _ rfl,
id                   └────────┘   └─┘
src  ─────────┘└────┘└────────┘└─┘└─┘└─
typ  ─────────┘└────┘└────────┘└─┘└─┘└─
doc  ─────────┘└────┘          └─┘   └─
txt  ─────────┘└────┘          └─┘   └─
par  ─────────┘└────┘          └─┘   └─
pid  ───────────────┘          └─┘   └─
st   ───────────────────────────────┘└─
238            rw function.funext_iff,
id                └─────────────────┘
src  ─────────┘└─┘└─────────────────┘└─
typ  ─────────┘└─┘└─────────────────┘└─
doc  ─────────┘└─┘                   └─
txt  ─────────┘└─┘                   └─
par  ─────────┘└─┘                   └─
pid  ────────────┘                   └─
st   ───────────────────────────────┘└─
239            apply h4
src  ─────────┘└────┘  
typ  ─────────┘└────┘  
doc  ─────────┘└────┘  
txt  ─────────┘└────┘  
par  ─────────┘└────┘  
pid  ───────────────┘  
st   ───────────────────
240          end
src  ───────┘└───
typ  ───────┘└───
doc  ───────┘└───
txt  ───────┘└───
par  ───────┘└───
pid  ────────────
st   ───────┘└─┘
241    ... = (-(a_n * sgm v b as n) + (sym_sym m b)
src  ─────┘                └┘           └─
typ  ─────┘                └┘           └─
doc  ─────┘                └┘           └─
txt  ─────┘                └┘           └─
par  ─────┘                └┘           └─
pid  ─────┘                └┘           └─
st   ───────────────────────────────────────────────
242          + coeffs.val_except n v (as.map (sym_sym m))) * m :
src  ───────┘                                    └──┘  └──
typ  ───────┘                                    └──┘  └──
doc  ───────┘                                    └──┘  └──
txt  ───────┘                                    └──┘  └──
par  ───────┘                                    └──┘  └──
pid  ───────┘                                    └──┘  └──
st   ────────────────────────────────────────────────────────────
243          begin
src  ───────┘     
typ  ───────┘     
doc  ───────┘     
txt  ───────┘     
par  ───────┘     
pid  ───────┘     
st   ───────┘└─────
244            simp only [add_mul _ _ m],
id                        └─────┘     
src  ─────────┘└─────────┘└─────┘└───┘ └─
typ  ─────────┘└─────────┘└─────┘└───┘└─
doc  ─────────┘└─────────┘       └───┘ └─
txt  ─────────┘└─────────┘       └───┘ └─
par  ─────────┘└─────────┘       └───┘ └─
pid  ────────────────────┘       └───┘ └──
st   ──────────────────────────────────┘└─
245            apply fun_mono_2, ring,
id                   └────────┘
src  ─────────┘└────┘└────────┘└┘└──┘└─
typ  ─────────┘└────┘└────────┘└┘└──┘└─
doc  ─────────┘└────┘          └┘└──┘└─
txt  ─────────┘└────┘          └┘└──┘└─
par  ─────────┘└────┘          └┘└──┘└─
pid  ───────────────┘          └───────
st   ─────────────────────────┘└────┘└─
246            simp only [coeffs.val_except, add_mul _ _ m],
id                        └───────────────┘  └─────┘     
src  ─────────┘└─────────┘└───────────────┘└┘└─────┘└───┘ └─
typ  ─────────┘└─────────┘└───────────────┘└┘└─────┘└───┘└─
doc  ─────────┘└─────────┘                 └┘       └───┘ └─
txt  ─────────┘└─────────┘                 └┘       └───┘ └─
par  ─────────┘└─────────┘                 └┘       └───┘ └─
pid  ────────────────────┘                 └┘       └───┘ └──
st   ─────────────────────────────────────────────────────┘└─
247            apply fun_mono_2,
id                   └────────┘
src  ─────────┘└────┘└────────┘└─
typ  ─────────┘└────┘└────────┘└─
doc  ─────────┘└────┘          └─
txt  ─────────┘└────┘          └─
par  ─────────┘└────┘          └─
pid  ───────────────┘          └─
st   ─────────────────────────┘└─
248            { rw [mul_comm _ m, ← coeffs.val_between_map_mul, list.map_map] },
id                   └──────┘       └────────────────────────┘  └──────────┘
src  ───────────┘└──┘└──────┘└─┘ └──┘└────────────────────────┘└┘└──────────┘└┘└──
typ  ───────────┘└──┘└──────┘└─┘└──┘└────────────────────────┘└┘└──────────┘└┘└──
doc  ───────────┘└──┘        └─┘ └──┘                          └┘            └┘└──
txt  ───────────┘└──┘        └─┘ └──┘                          └┘            └┘└──
par  ───────────┘└──┘        └─┘ └──┘                          └┘            └┘└──
pid  ───────────────┘        └─┘ └──┘                          └┘            └────
st   ──────────┘└───────────────┘└────────────────────────────┘└────────────┘└─
249            simp only [list.length_map, mul_comm _ m],
id                        └─────────────┘  └──────┘   
src  ─────────┘└─────────┘└─────────────┘└┘└──────┘└─┘ └─
typ  ─────────┘└─────────┘└─────────────┘└┘└──────┘└─┘└─
doc  ─────────┘└─────────┘               └┘        └─┘ └─
txt  ─────────┘└─────────┘               └┘        └─┘ └─
par  ─────────┘└─────────┘               └┘        └─┘ └─
pid  ────────────────────┘               └┘        └─┘ └──
st   ──────────────────────────────────────────────────┘└─
250            rw [← coeffs.val_between_map_mul, list.map_map]
id                   └────────────────────────┘  └──────────┘
src  ─────────┘└────┘└────────────────────────┘└┘└──────────┘└─
typ  ─────────┘└────┘└────────────────────────┘└┘└──────────┘└─
doc  ─────────┘└────┘                          └┘            └─
txt  ─────────┘└────┘                          └┘            └─
par  ─────────┘└────┘                          └┘            └─
pid  ───────────────┘                          └┘            └─
st   ─────────────────────────────────────────┘└────────────┘
251          end
src  ───────┘└───
typ  ───────┘└───
doc  ───────┘└───
txt  ───────┘└───
par  ───────┘└───
pid  ────────────
st   ───────┘└─┘
252    ... = (sym_sym m b + (coeffs.val_except n v (as.map (sym_sym m)) +
src  ─────┘                                                └─┘ 
typ  ─────┘                                                └─┘ 
doc  ─────┘                                                └─┘ 
txt  ─────┘                                                └─┘ 
par  ─────┘                                                └─┘ 
pid  ─────┘                                                └─┘ 
st   ─────────────────────────────────────────────────────────────────────
253            (-a_n * sgm v b as n))) * m : by ring
id              
src  ─────────┘             └──┘  └─┘  └────
typ  ─────────┘             └──┘  └─┘  └────
doc  ─────────┘              └──┘  └─┘  └────
txt  ─────────┘              └──┘  └─┘  └────
par  ─────────┘              └──┘  └─┘  └────
pid  ─────────┘              └──┘  └─┘  └─────
st   ─────────────────────────────────────────┘└─────
254    ... = (term.val (v ⟨n ↦ sgm v b as n⟩) (coeffs_reduce n b as)) * m :
id                                             └───────────┘
src  ─┘└──┘                        └┘ └───────────┘    └─┘  └──
typ  ─┘└──┘                        └┘ └───────────┘    └─┘  └──
doc  ─┘└──┘                        └┘                  └─┘  └──
txt  ─┘└──┘                        └┘                  └─┘  └──
par  ─┘└──┘                        └┘                  └─┘  └──
pid  ─────┘                        └┘                  └─┘  └──
st   ─┘└────────────────────────────────────────────────────────────────────
255          begin
src  ───────┘     
typ  ───────┘     
doc  ───────┘     
txt  ───────┘     
par  ───────┘     
pid  ───────┘     
st   ───────┘└─────
256            simp only [coeffs_reduce, term.val, m, a_n],
id                        └───────────┘  └──────┘    └─┘
src  ─────────┘└─────────┘└───────────┘└┘└──────┘└┘ └┘   └─
typ  ─────────┘└─────────┘└───────────┘└┘└──────┘└┘└┘└─┘└─
doc  ─────────┘└─────────┘             └┘        └┘ └┘   └─
txt  ─────────┘└─────────┘             └┘        └┘ └┘   └─
par  ─────────┘└─────────┘             └┘        └┘ └┘   └─
pid  ────────────────────┘             └┘        └┘ └┘   └──
st   ────────────────────────────────────────────────────┘└─
257            rw [← coeffs.val_except_add_eq n,
id                   └──────────────────────┘ 
src  ─────────┘└────┘└──────────────────────┘ └─
typ  ─────────┘└────┘└──────────────────────┘└─
doc  ─────────┘└────┘                         └─
txt  ─────────┘└────┘                         └─
par  ─────────┘└────┘                         └─
pid  ───────────────┘                         └─
st   ─────────────────────────────────────────┘└─
258              coeffs.val_except_update_set, get_set, update_eq]
id               └──────────────────────────┘  └─────┘  └───────┘
src  ───────────┘└──────────────────────────┘└┘└─────┘└┘└───────┘└─
typ  ───────────┘└──────────────────────────┘└┘└─────┘└┘└───────┘└─
doc  ───────────┘                            └┘       └┘         └─
txt  ───────────┘                            └┘       └┘         └─
par  ───────────┘                            └┘       └┘         └─
pid  ───────────┘                            └┘       └┘         └─
st   ───────────────────────────────────────┘└───────┘└─────────┘
259          end,
src  ───────┘└─┘
typ  ───────┘└─┘
doc  ───────┘└─┘
txt  ───────┘└─┘
par  ───────┘└─┘
pid  ──────────┘
st   ───────┘└─┘└─
260    rw [← int.mul_div_cancel (term.val _ _) h3, ← h4, int.zero_div]
id           └────────────────┘  └──────┘      └┘    └┘  └──────────┘
src    └────┘└────────────────┘ └──────┘└────┘  └──┘  └┘└──────────┘└┘
typ    └────┘└────────────────┘ └──────┘└────┘└┘└──┘└┘└┘└──────────┘└┘
doc    └────┘                           └────┘  └──┘  └┘            └┘
txt    └────┘                           └────┘  └──┘  └┘            └┘
par    └────┘                           └────┘  └──┘  └┘            └┘
pid      └──┘                           └────┘  └──┘  └┘            
st   ───────────────────────────────────────────┘└────┘└────────────┘
261  end
st   └─┘
262  
263  -- Requires : t1.coeffs[m] = 1
264  def cancel (m : nat) (t1 t2 : term) : term :=
id                   └─┘           └──┘    └──┘
src                  └─┘           └──┘    └──┘
typ                  └─┘           └──┘    └──┘
265  term.add (t1.mul (-(get m (t2.snd)))) t2
id   └──────┘  └┘└──┘   └─┘   └┘└──┘     └┘
src  └──────┘    └──┘   └─┘      └──┘
typ  └──────┘  └┘└──┘   └─┘   └┘└──┘     └┘
266  
267  def subst (n : nat) (t1 t2 : term) : term :=
id                  └─┘           └──┘    └──┘
src                 └─┘           └──┘    └──┘
typ                 └─┘           └──┘    └──┘
268  term.add (t1.mul (get n t2.snd)) (t2.fst, t2.snd {n ↦ 0})
id   └──────┘  └┘└──┘  └─┘  └┘└──┘   └┘└──┘  └┘└──┘    
src  └──────┘    └──┘  └─┘     └──┘     └──┘    └──┘     
typ  └──────┘  └┘└──┘  └─┘  └┘└──┘   └┘└──┘  └┘└──┘    
269  
270  lemma subst_correct {v : nat → int} {b : int}
id                            └─┘   └─┘       └─┘
src                           └─┘   └─┘       └─┘
typ                           └─┘   └─┘       └─┘
271   {as : list int} {t : term} {n : nat} :
id          └──┘ └─┘       └──┘       └─┘
src         └──┘ └─┘       └──┘       └─┘
typ         └──┘ └─┘       └──┘       └─┘
272    0 < get n as → 0 = term.val v (b,as) →
id        └─┘  └┘      └──────┘   └┘
src       └─┘           └──────┘   
typ       └─┘  └┘      └──────┘   └┘
273    term.val v t = term.val (v ⟨n ↦ sgm v b as n⟩) (subst n (rhs n b as) t) :=
id     └──────┘    └──────┘     └─┘   └┘    └───┘   └─┘   └┘  
src    └──────┘      └──────┘       └─┘            └───┘    └─┘
typ    └──────┘    └──────┘     └─┘   └┘    └───┘   └─┘   └┘  
274  begin
st   └─────
275    intros h1 h2,
src    └──────────┘
typ    └──────────┘
doc    └──────────┘
txt    └──────────┘
par    └──────────┘
pid          └────┘
st   ─────────────┘└─
276    simp only [subst, term.val, term.val_add, term.val_mul],
id                └───┘  └──────┘  └──────────┘  └──────────┘
src    └─────────┘└───┘└┘└──────┘└┘└──────────┘└┘└──────────┘
typ    └─────────┘└───┘└┘└──────┘└┘└──────────┘└┘└──────────┘
doc    └─────────┘     └┘        └┘            └┘            
txt    └─────────┘     └┘        └┘            └┘            
par    └─────────┘     └┘        └┘            └┘            
pid        └──┘└┘     └┘        └┘            └┘            
st   ────────────────────────────────────────────────────────┘└─
277    rw ← rhs_correct _ h1 h2,
id          └─────────┘   └┘ └┘
src    └───┘└─────────┘└─┘  
typ    └───┘└─────────┘└─┘└┘└┘
doc    └───┘           └─┘  
txt    └───┘           └─┘  
par    └───┘           └─┘  
pid      └─┘           └─┘  
st   ─────────────────────────┘└─
278    cases t with b' as',
id           
src    └────┘ └──────────┘
typ    └────┘└──────────┘
doc    └────┘ └──────────┘
txt    └────┘ └──────────┘
par    └────┘ └──────────┘
pid          └──────────┘
st   ────────────────────┘└─
279    simp only [term.val],
id                └──────┘
src    └─────────┘└──────┘
typ    └─────────┘└──────┘
doc    └─────────┘        
txt    └─────────┘        
par    └─────────┘        
pid        └──┘└┘        
st   ─────────────────────┘└─
280    have h3 : coeffs.val (v ⟨n ↦ sgm v b as n⟩) (as' {n ↦ 0}) =
id               └────────┘         └─┘    └┘                
src    └────────┘└────────┘     └─┘      └┘     └┘└┘
typ    └────────┘└────────┘     └─┘ └┘  └┘     └┘└┘
doc    └────────┘                        └┘       └┘ └┘ 
txt    └────────┘                        └┘       └┘ └┘ 
par    └────────┘                        └┘       └┘ └┘ 
pid    └─────┘└─┘                        └┘       └┘ └┘ 
st   ──────────────────────────────────────────────────────────────
281      coeffs.val_except n v as',
id       └───────────────┘   └─┘
src  ───┘└───────────────┘  
typ  ───┘└───────────────┘└─┘
doc  ───┘                   
txt  ───┘                   
par  ───┘                   
pid  ───┘                   
st   ────────────────────────────┘└─
282    { rw [← coeffs.val_except_add_eq n, get_set,
id             └──────────────────────┘   └─────┘
src      └────┘└──────────────────────┘ └┘└─────┘└─
typ      └────┘└──────────────────────┘└┘└─────┘└─
doc      └────┘                         └┘       └─
txt      └────┘                         └┘       └─
par      └────┘                         └┘       └─
pid        └──┘                         └┘       └─
st   ───┘└──────────────────────────────┘└───────┘└─
283        zero_mul, add_zero, coeffs.val_except_update_set] },
id         └──────┘  └──────┘  └──────────────────────────┘
src  ─────┘└──────┘└┘└──────┘└┘└──────────────────────────┘└┘
typ  ─────┘└──────┘└┘└──────┘└┘└──────────────────────────┘└┘
doc  ─────┘        └┘        └┘                            └┘
txt  ─────┘        └┘        └┘                            └┘
par  ─────┘        └┘        └┘                            └┘
pid  ─────┘        └┘        └┘                            
st   ─────────────┘└────────┘└────────────────────────────┘└┘
284    rw [h3, ← coeffs.val_except_add_eq n], ring
id         └┘    └──────────────────────┘ 
src    └──┘  └──┘└──────────────────────┘   └───┘
typ    └──┘└┘└──┘└──────────────────────┘  └───┘
doc    └──┘  └──┘                           └───┘
txt    └──┘  └──┘                           └───┘
par    └──┘  └──┘                           └───┘
pid      └┘  └──┘                               
st   ───────┘└────────────────────────────┘└──────┘
285  end
st   └─┘
286  
287  /- The type of equality elimination rules. -/
288  
289  @[derive has_reflect, derive inhabited]
id            └─────────┘         └───────┘
src           └─────────┘         └───────┘
typ           └─────────┘         └───────┘
doc    └────┘              └────┘
290  inductive ee : Type
291  | drop   : ee
292  | nondiv : int → ee
id              └─┘
src             └─┘
typ             └─┘
293  | factor : int → ee
id              └─┘
src             └─┘
typ             └─┘
294  | neg    : ee
295  | reduce : nat → ee
id              └─┘
src             └─┘
typ             └─┘
296  | cancel : nat → ee
id              └─┘
src             └─┘
typ             └─┘
297  
298  namespace ee
299  
300  def repr : ee → string
id              └┘  └────┘
src             └┘  └────┘
typ             └┘  └────┘
301  | drop   := "↓"
id     └──┘
src    └──┘
typ    └──┘
302  | (nondiv i) := i.repr ++ "∤"
id      └────┘       └───┘ └┘
src     └────┘        └───┘ └┘
typ     └────┘       └───┘ └┘
303  | (factor i) := "/" ++ i.repr
id      └────┘          └┘  └───┘
src     └────┘           └┘  └───┘
typ     └────┘          └┘  └───┘
304  | neg    := "-"
id     └─┘
src    └─┘
typ    └─┘
305  | (reduce n) := "≻" ++ n.repr
id      └────┘          └┘  └───┘
src     └────┘           └┘  └───┘
typ     └────┘          └┘  └───┘
306  | (cancel n) := "+" ++ n.repr
id      └────┘          └┘  └───┘
src     └────┘           └┘  └───┘
typ     └────┘          └┘  └───┘
307  
308  instance has_repr : has_repr ee := ⟨repr⟩
id                       └──────┘ └┘     └──┘
src                      └──────┘ └┘     └──┘
typ                      └──────┘ └┘     └──┘
309  
310  meta instance has_to_format : has_to_format ee := ⟨λ x, x.repr⟩
id                                 └───────────┘ └┘         └───┘
src                                └───────────┘ └┘           └───┘
typ                                └───────────┘ └┘         └───┘
311  
312  end ee
313  
314  def eq_elim : list ee → clause → clause
id                 └──┘ └┘  └────┘   └────┘
src                └──┘ └┘   └────┘   └────┘
typ                └──┘ └┘  └────┘   └────┘
315  | []     ([], les)     := ([],les)
id     └┘     └┘  └─┘         └┘
src    └┘     └┘              └┘
typ    └┘     └┘  └─┘         └┘
316  | []     ((_::_), les) := ([],[])
id     └┘       └┘            └┘ └┘
src    └┘       └┘            └┘ └┘
typ    └┘       └┘            └┘ └┘
317  | (_::_) ([], les)     := ([],[])
id       └┘   └┘              └┘ └┘
src      └┘   └┘              └┘ └┘
typ      └┘   └┘              └┘ └┘
318  | (ee.drop::es) ((eq::eqs), les) := eq_elim es (eqs, les)
id      └─────┘└┘└┘     └┘└─┘   └─┘     └─────┘    
src     └─────┘└┘       └┘                         
typ     └─────┘└┘└┘     └┘└─┘   └─┘     └─────┘    
319  | (ee.neg::es)  ((eq::eqs), les) := eq_elim es ((eq.neg::eqs), les)
id      └────┘└┘└┘    └┘└┘└─┘   └─┘     └─────┘       └──┘└┘
src     └────┘└┘      └┘└┘                            └──┘└┘
typ     └────┘└┘└┘    └┘└┘└─┘   └─┘     └─────┘       └──┘└┘
320  | (ee.nondiv i::es) ((b,as)::eqs, les) :=
id      └───────┘ └┘    └┘ └┘ └┘
src     └───────┘  └┘    └┘     └┘
typ     └───────┘ └┘    └┘ └┘ └┘
321    if ¬(i ∣ b) ∧ (∀ x ∈ as, i ∣ x)
id                             
src                           
typ                            
322    then ([],[⟨-1,[]⟩])
id          └┘    └┘ 
src         └┘    └┘ 
typ         └┘    └┘ 
323    else ([],[])
id          └┘ └┘
src         └┘ └┘
typ         └┘ └┘
324  | (ee.factor i::es) ((b,as)::eqs, les) :=
id      └───────┘ └┘└┘  └┘ └┘ └┘└─┘  └─┘
src     └───────┘  └┘    └┘     └┘
typ     └───────┘ └┘└┘  └┘ └┘ └┘└─┘  └─┘
325    if (i ∣ b) ∧ (∀ x ∈ as, i ∣ x)
id                             
src                            
typ                            
326    then eq_elim es ((term.div i (b,as)::eqs), les)
id          └─────┘     └──────┘        └┘
src                     └──────┘        └┘
typ         └─────┘     └──────┘        └┘
327    else ([],[])
id          └┘ └┘
src         └┘ └┘
typ         └┘ └┘
328  | (ee.reduce n::es) ((b,as)::eqs, les) :=
id      └───────┘ └┘└┘  └┘ └┘ └┘└─┘  └─┘
src     └───────┘  └┘    └┘     └┘
typ     └───────┘ └┘└┘  └┘ └┘ └┘└─┘  └─┘
329    if 0 < get n as
id           └─┘
src          └─┘
typ          └─┘
330    then let eq' := coeffs_reduce n b as in
id              └─┘    └───────────┘
src                    └───────────┘
typ             └─┘    └───────────┘
331         let r := rhs n b as in
id                  └─┘
src                  └─┘
typ                 └─┘
332         let eqs' := eqs.map (subst n r) in
id              └──┘       └──┘  └───┘   
src                        └──┘  └───┘
typ             └──┘       └──┘  └───┘   
333         let les' := les.map (subst n r) in
id              └──┘       └──┘  └───┘   
src                        └──┘  └───┘
typ             └──┘       └──┘  └───┘   
334         eq_elim es ((eq'::eqs'), les')
id          └─────┘     └─┘└┘└──┘   └──┘
src                        └┘
typ         └─────┘     └─┘└┘└──┘   └──┘
335    else ([],[])
id          └┘ └┘
src         └┘ └┘
typ         └┘ └┘
336  | (ee.cancel m::es) ((eq::eqs), les)  :=
id      └───────┘ └┘└┘   └┘└┘└─┘   └─┘
src     └───────┘  └┘     └┘└┘
typ     └───────┘ └┘└┘   └┘└┘└─┘   └─┘
337    eq_elim es ((eqs.map (cancel m eq)), (les.map (cancel m eq)))
id     └─────┘        └──┘  └────┘             └──┘  └────┘
src                   └──┘  └────┘             └──┘  └────┘
typ    └─────┘        └──┘  └────┘             └──┘  └────┘
338  
339  open tactic
340  
341  lemma sat_empty : clause.sat ([],[]) :=
id                     └────────┘ └┘ └┘
src                    └────────┘ └┘ └┘
typ                    └────────┘ └┘ └┘
342  ⟨λ _,0, ⟨dec_trivial, dec_trivial⟩⟩
id           └─────────┘  └─────────┘
src           └─────────┘  └─────────┘
typ          └─────────┘  └─────────┘
doc           └─────────┘  └─────────┘
343  
344  lemma sat_eq_elim :
345    ∀ {es : list ee} {c : clause}, c.sat → (eq_elim es c).sat
id            └──┘ └┘       └────┘   └──┘    └─────┘ └┘  └─┘
src            └──┘ └┘       └────┘    └──┘    └─────┘      └─┘
typ           └──┘ └┘       └────┘   └──┘    └─────┘ └┘  └─┘
346  | []     ([], les) h := h
id     └┘     └┘       
src    └┘     └┘
typ    └┘     └┘       
347  | (e::_) ([], les) h :=
id       └┘   └┘
src      └┘   └┘
typ      └┘   └┘
348    by {cases e; simp only [eq_elim]; apply sat_empty}
id                            └─────┘         └───────┘
src        └────┘   └─────────┘└─────┘  └────┘└───────┘
typ        └────┘  └─────────┘└─────┘  └────┘└───────┘
doc        └────┘   └─────────┘         └────┘
txt        └────┘   └─────────┘         └────┘
par        └────┘   └─────────┘         └────┘
pid                    └──┘└┘              
st       └─────────────────────────────────────────────┘└┘
349  | [] ((_::_), les) h := sat_empty
id     └┘   └┘              └───────┘
src    └┘   └┘              └───────┘
typ    └┘   └┘              └───────┘
350  | (ee.drop::es) ((eq::eqs), les) h1 :=
id      └─────┘└┘       └┘
src     └─────┘└┘       └┘
typ     └─────┘└┘       └┘
351    begin
st     └─────
352      apply (@sat_eq_elim es _ _),
id               └─────────┘ └┘
src      └────┘               └───┘
typ      └────┘  └─────────┘└┘└───┘
doc      └────┘               └───┘
txt      └────┘               └───┘
par      └────┘               └───┘
pid                          └───┘
st   ──────────────────────────────┘└─
353      rcases h1 with ⟨v,h1,h2⟩,
id              └┘
src      └─────┘  └─────────────┘
typ      └─────┘└┘└─────────────┘
doc      └─────┘  └─────────────┘
txt      └─────┘  └─────────────┘
par      └─────┘  └─────────────┘
pid              └─────────────┘
st   ───────────────────────────┘└─
354      refine ⟨v, list.forall_mem_of_forall_mem_cons h1, h2⟩
id                 └────────────────────────────────┘ └┘  └┘
src      └─────┘  └┘└────────────────────────────────┘  └┘  └─
typ      └─────┘ └┘└────────────────────────────────┘└┘└┘└┘└─
doc      └─────┘  └┘                                    └┘  └─
txt      └─────┘  └┘                                    └┘  └─
par      └─────┘  └┘                                    └┘  └─
pid              └┘                                    └┘  
st   ──────────────────────────────────────────────────────────
355    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
356  | (ee.neg::es) ((eq::eqs), les) h1 :=
id      └────┘└┘       └┘
src     └────┘└┘       └┘
typ     └────┘└┘       └┘
357    begin
st     └─────
358      simp only [eq_elim], apply sat_eq_elim,
id                  └─────┘
src      └─────────┘└─────┘  └────┘
typ      └─────────┘└─────┘  └────┘
doc      └─────────┘         └────┘
txt      └─────────┘         └────┘
par      └─────────┘         └────┘
pid          └──┘└┘              
st   ──────────────────────┘└─────────────────┘└─
359      cases h1 with v h1,
id             └┘
src      └────┘  └────────┘
typ      └────┘└┘└────────┘
doc      └────┘  └────────┘
txt      └────┘  └────────┘
par      └────┘  └────────┘
pid             └────────┘
st   ─────────────────────┘└─
360      existsi v,
id               
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid             
st   ────────────┘└─
361      cases h1 with hl hr,
id             └┘
src      └────┘  └─────────┘
typ      └────┘└┘└─────────┘
doc      └────┘  └─────────┘
txt      └────┘  └─────────┘
par      └────┘  └─────────┘
pid             └─────────┘
st   ──────────────────────┘└─
362      apply and.intro _ hr,
id             └───────┘   └┘
src      └────┘└───────┘└─┘
typ      └────┘└───────┘└─┘└┘
doc      └────┘         └─┘
txt      └────┘         └─┘
par      └────┘         └─┘
pid                    └─┘
st   ───────────────────────┘└─
363      rw list.forall_mem_cons at *,
id          └──────────────────┘
src      └─┘└──────────────────┘└───┘
typ      └─┘└──────────────────┘└───┘
doc      └─┘                    └───┘
txt      └─┘                    └───┘
par      └─┘                    └───┘
pid                            └───┘
st   ───────────────────────────────┘└─
364      apply and.intro _ hl.right,
id             └───────┘   └──────┘
src      └────┘└───────┘└─┘└──────┘
typ      └────┘└───────┘└─┘└──────┘
doc      └────┘         └─┘
txt      └────┘         └─┘
par      └────┘         └─┘
pid                    └─┘
st   ─────────────────────────────┘└─
365      rw term.val_neg,
id          └──────────┘
src      └─┘└──────────┘
typ      └─┘└──────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ──────────────────┘└─
366      rw ← hl.left,
src      └───┘
typ      └───┘└─────┘
doc      └───┘
txt      └───┘
par      └───┘
pid        └─┘
st   ───────────────┘└─
367      refl
src      └────
typ      └────
doc      └────
txt      └────
par      └────
pid          
st   ─────────
368    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
369  | (ee.nondiv i::es) ((b,as)::eqs, les) h1 :=
id      └───────┘  └┘    └┘     └┘
src     └───────┘  └┘    └┘     └┘
typ     └───────┘  └┘    └┘     └┘
370    begin
st     └─────
371      unfold eq_elim,
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid            └──────┘
st   ─────────────────┘└─
372      by_cases h2 : (¬i ∣ b ∧ ∀ (x : ℤ), x ∈ as → i ∣ x),
id                                           └┘   
src      └───────┘  └─┘      └────┘         
typ      └───────┘  └─┘     └────┘   └┘   
doc      └───────┘  └─┘       └────┘          
txt      └───────┘  └─┘       └────┘          
par      └───────┘  └─┘       └────┘          
pid                └─┘       └────┘          
st   ─────────────────────────────────────────────────────┘└─
373      { exfalso, cases h1 with v h1,
id                        └┘
src        └─────┘  └────┘  └────────┘
typ        └─────┘  └────┘└┘└────────┘
doc        └─────┘  └────┘  └────────┘
txt        └─────┘  └────┘  └────────┘
par        └─────┘  └────┘  └────────┘
pid                        └────────┘
st   ─────┘└─────┘└──────────────────┘└─
374        have h3 : 0 = b + coeffs.val v as := h1.left _ (or.inl rfl),
id                        └────────┘  └┘    └─────┘    └────┘ └─┘
src        └──────────┘ └────────┘   └──┘└─────┘└─┘ └────┘└─┘
typ        └──────────┘└────────┘└┘└──┘└─────┘└─┘ └────┘└─┘
doc        └──────────┘                └──┘       └─┘          
txt        └──────────┘                └──┘       └─┘          
par        └──────────┘                └──┘       └─┘          
pid        └─────┘└───┘                └──┘       └─┘          
st   ────────────────────────────────────────────────────────────────┘└─
375        have h4 : i ∣ coeffs.val v as     := coeffs.dvd_val h2.right,
id                      └────────┘  └┘        └────────────┘ └──────┘
src        └────────┘  └────────┘   └──────┘└────────────┘└──────┘
typ        └────────┘ └────────┘└┘└──────┘└────────────┘└──────┘
doc        └────────┘               └──────┘              
txt        └────────┘               └──────┘              
par        └────────┘               └──────┘              
pid        └─────┘└─┘               └──────┘              
st   ─────────────────────────────────────────────────────────────────┘└─
376        have h5 : i ∣ b + coeffs.val v as := by { rw ← h3, apply dvd_zero },
id                         └────────┘  └┘              └┘        └──────┘
src        └────────┘    └────────┘   └──┘  └─┘└───┘  └┘└────┘└──────┘
typ        └────────┘  └────────┘└┘└──┘  └─┘└───┘└┘└┘└────┘└──────┘
doc        └────────┘                 └──┘  └─┘└───┘  └┘└────┘        
txt        └────────┘                 └──┘  └─┘└───┘  └┘└────┘        
par        └────────┘                 └──┘  └─┘└───┘  └┘└────┘        
pid        └─────┘└─┘                 └──┘  └──────┘  └──────┘        └┘
st   ────────────────────────────────────────────┘└────────┘└───────────────┘└┘
377        rw ← dvd_add_iff_left h4 at h5, apply h2.left h5 },
id              └──────────────┘ └┘              └─────┘ └┘
src        └───┘└──────────────┘  └────┘  └────┘└─────┘  
typ        └───┘└──────────────┘└┘└────┘  └────┘└─────┘└┘
doc        └───┘                  └────┘  └────┘         
txt        └───┘                  └────┘  └────┘         
par        └───┘                  └────┘  └────┘         
pid          └─┘                  └────┘                
st   ───────────────────────────────────┘└─────────────────┘└┘
378      rw if_neg h2, apply sat_empty
id          └────┘ └┘        └───────┘
src      └─┘└────┘    └────┘└───────┘
typ      └─┘└────┘└┘  └────┘└───────┘
doc      └─┘          └────┘         
txt      └─┘          └────┘         
par      └─┘          └────┘         
pid                                
st   ───────────────┘└─────────────────
379    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
380  | (ee.factor i::es) ((b,as)::eqs, les) h1 :=
id      └───────┘  └┘    └┘     └┘
src     └───────┘  └┘    └┘     └┘
typ     └───────┘  └┘    └┘     └┘
381    begin
st     └─────
382      simp only [eq_elim],
id                  └─────┘
src      └─────────┘└─────┘
typ      └─────────┘└─────┘
doc      └─────────┘       
txt      └─────────┘       
par      └─────────┘       
pid          └──┘└┘       
st   ──────────────────────┘└─
383      by_cases h2 : (i ∣ b) ∧ (∀ x ∈ as, i ∣ x),
id                                     └┘  
src      └───────┘  └─┘    └┘   └───┘      
typ      └───────┘  └─┘   └┘   └───┘└┘   
doc      └───────┘  └─┘    └┘   └───┘      
txt      └───────┘  └─┘    └┘   └───┘      
par      └───────┘  └─┘    └┘   └───┘      
pid                └─┘    └┘   └───┘      
st   ────────────────────────────────────────────┘└─
384      { rw if_pos h2, apply sat_eq_elim, cases h1 with v h1,
id            └────┘ └┘                           └┘
src        └─┘└────┘    └────┘             └────┘  └────────┘
typ        └─┘└────┘└┘  └────┘             └────┘└┘└────────┘
doc        └─┘          └────┘             └────┘  └────────┘
txt        └─┘          └────┘             └────┘  └────────┘
par        └─┘          └────┘             └────┘  └────────┘
pid                                             └────────┘
st   ─────┘└──────────┘└─────────────────┘└──────────────────┘└─
385        existsi v, cases h1 with h3 h4, apply and.intro _ h4,
id                         └┘                   └───────┘   └┘
src        └──────┘   └────┘  └─────────┘  └────┘└───────┘└─┘
typ        └──────┘  └────┘└┘└─────────┘  └────┘└───────┘└─┘└┘
doc        └──────┘   └────┘  └─────────┘  └────┘         └─┘
txt        └──────┘   └────┘  └─────────┘  └────┘         └─┘
par        └──────┘   └────┘  └─────────┘  └────┘         └─┘
pid                         └─────────┘                └─┘
st   ──────────────┘└───────────────────┘└────────────────────┘└─
386        rw list.forall_mem_cons at *, cases h3 with h5 h6,
id            └──────────────────┘             └┘
src        └─┘└──────────────────┘└───┘  └────┘  └─────────┘
typ        └─┘└──────────────────┘└───┘  └────┘└┘└─────────┘
doc        └─┘                    └───┘  └────┘  └─────────┘
txt        └─┘                    └───┘  └────┘  └─────────┘
par        └─┘                    └───┘  └────┘  └─────────┘
pid                              └───┘         └─────────┘
st   ─────────────────────────────────┘└───────────────────┘└─
387        apply and.intro _ h6,
id               └───────┘   └┘
src        └────┘└───────┘└─┘
typ        └────┘└───────┘└─┘└┘
doc        └────┘         └─┘
txt        └────┘         └─┘
par        └────┘         └─┘
pid                      └─┘
st   ─────────────────────────┘└─
388        rw [term.val_div h2.left h2.right, ← h5, int.zero_div] },
id             └──────────┘ └─────┘ └──────┘    └┘  └──────────┘
src        └──┘└──────────┘└─────┘└──────┘└──┘  └┘└──────────┘└┘
typ        └──┘└──────────┘└─────┘└──────┘└──┘└┘└┘└──────────┘└┘
doc        └──┘                           └──┘  └┘            └┘
txt        └──┘                           └──┘  └┘            └┘
par        └──┘                           └──┘  └┘            └┘
pid          └┘                           └──┘  └┘            
st   ──────────────────────────────────────┘└────┘└────────────┘└┘
389      { rw if_neg h2, apply sat_empty }
id            └────┘ └┘        └───────┘
src        └─┘└────┘    └────┘└───────┘
typ        └─┘└────┘└┘  └────┘└───────┘
doc        └─┘          └────┘         
txt        └─┘          └────┘         
par        └─┘          └────┘         
pid                                  
st   ─────────────────┘└────────────────┘└─
390    end
st   ────┘
391  | (ee.reduce n::es) ((b,as)::eqs, les) h1 :=
id      └───────┘  └┘    └┘     └┘
src     └───────┘  └┘    └┘     └┘
typ     └───────┘  └┘    └┘     └┘
392    begin
st     └─────
393      simp only [eq_elim],
id                  └─────┘
src      └─────────┘└─────┘
typ      └─────────┘└─────┘
doc      └─────────┘       
txt      └─────────┘       
par      └─────────┘       
pid          └──┘└┘       
st   ──────────────────────┘└─
394      by_cases h2 : 0 < get n as,
id                        └─┘  └┘
src      └───────┘  └───┘└─┘ 
typ      └───────┘  └───┘└─┘└┘
doc      └───────┘  └───┘     
txt      └───────┘  └───┘     
par      └───────┘  └───┘     
pid                └───┘     
st   ─────────────────────────────┘└─
395      tactic.rotate 1,
id       └───────────┘
src      └───────────┘
typ      └───────────┘
par      └───────────┘
st   ─────────────────┘└──
396      { rw if_neg h2, apply sat_empty },
id            └────┘ └┘        └───────┘
src        └─┘└────┘    └────┘└───────┘
typ        └─┘└────┘└┘  └────┘└───────┘
doc        └─┘          └────┘         
txt        └─┘          └────┘         
par        └─┘          └────┘         
pid                                  
st   ─────┘└──────────┘└────────────────┘└┘
397      rw if_pos h2,
id          └────┘ └┘
src      └─┘└────┘
typ      └─┘└────┘└┘
doc      └─┘      
txt      └─┘      
par      └─┘      
pid              
st   ───────────────┘└─
398      apply sat_eq_elim,
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ────────────────────┘└─
399      cases h1 with v h1,
id             └┘
src      └────┘  └────────┘
typ      └────┘└┘└────────┘
doc      └────┘  └────────┘
txt      └────┘  └────────┘
par      └────┘  └────────┘
pid             └────────┘
st   ─────────────────────┘└─
400      existsi v ⟨n ↦ sgm v b as n⟩,
id                   └─┘    └┘ 
src      └──────┘  └─┘     
typ      └──────┘ └─┘ └┘
doc      └──────┘           
txt      └──────┘           
par      └──────┘           
pid                        
st   ───────────────────────────────┘└─
401      cases h1 with h1 h3,
id             └┘
src      └────┘  └─────────┘
typ      └────┘└┘└─────────┘
doc      └────┘  └─────────┘
txt      └────┘  └─────────┘
par      └────┘  └─────────┘
pid             └─────────┘
st   ──────────────────────┘└─
402      rw list.forall_mem_cons at h1,
id          └──────────────────┘
src      └─┘└──────────────────┘└────┘
typ      └─┘└──────────────────┘└────┘
doc      └─┘                    └────┘
txt      └─┘                    └────┘
par      └─┘                    └────┘
pid                            └────┘
st   ────────────────────────────────┘└─
403      cases h1 with h4 h5,
id             └┘
src      └────┘  └─────────┘
typ      └────┘└┘└─────────┘
doc      └────┘  └─────────┘
txt      └────┘  └─────────┘
par      └────┘  └─────────┘
pid             └─────────┘
st   ──────────────────────┘└─
404      constructor,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
st   ──────────────┘└─
405      { rw list.forall_mem_cons,
id            └──────────────────┘
src        └─┘└──────────────────┘
typ        └─┘└──────────────────┘
doc        └─┘
txt        └─┘
par        └─┘
pid          
st   ─────┘└─────────────────────┘└─
406        constructor,
src        └─────────┘
typ        └─────────┘
doc        └─────────┘
txt        └─────────┘
par        └─────────┘
st   ────────────────┘└─
407        { apply coeffs_reduce_correct h2 h4 },
id                 └───────────────────┘ └┘ └┘
src          └────┘└───────────────────┘    
typ          └────┘└───────────────────┘└┘└┘
doc          └────┘                         
txt          └────┘                         
par          └────┘                         
pid                                        
st   ───────┘└────────────────────────────────┘└┘
408        { intros x h6, rw list.mem_map at h6,
id                           └──────────┘
src          └─────────┘  └─┘└──────────┘└────┘
typ          └─────────┘  └─┘└──────────┘└────┘
doc          └─────────┘  └─┘            └────┘
txt          └─────────┘  └─┘            └────┘
par          └─────────┘  └─┘            └────┘
pid                └───┘                └────┘
st   ──────────────────┘└─────────────────────┘└─
409          cases h6 with t h6, cases h6 with h6 h7,
id                 └┘                  └┘
src          └────┘  └────────┘  └────┘  └─────────┘
typ          └────┘└┘└────────┘  └────┘└┘└─────────┘
doc          └────┘  └────────┘  └────┘  └─────────┘
txt          └────┘  └────────┘  └────┘  └─────────┘
par          └────┘  └────────┘  └────┘  └─────────┘
pid                 └────────┘         └─────────┘
st   ─────────────────────────┘└───────────────────┘└─
410          rw [← h7, ← subst_correct h2 h4], apply h5 _ h6 } },
id                 └┘    └───────────┘ └┘ └┘         └┘   └┘
src          └────┘  └──┘└───────────┘      └────┘  └─┘  
typ          └────┘└┘└──┘└───────────┘└┘└┘  └────┘└┘└─┘└┘
doc          └────┘  └──┘                   └────┘  └─┘  
txt          └────┘  └──┘                   └────┘  └─┘  
par          └────┘  └──┘                   └────┘  └─┘  
pid            └──┘  └──┘                          └─┘  
st   ───────────────┘└─────────────────────┘└───────────────┘└──┘
411      { intros x h6, rw list.mem_map at h6,
id                         └──────────┘
src        └─────────┘  └─┘└──────────┘└────┘
typ        └─────────┘  └─┘└──────────┘└────┘
doc        └─────────┘  └─┘            └────┘
txt        └─────────┘  └─┘            └────┘
par        └─────────┘  └─┘            └────┘
pid              └───┘                └────┘
st   ────────────────┘└─────────────────────┘└─
412        cases h6 with t h6, cases h6 with h6 h7,
id               └┘                  └┘
src        └────┘  └────────┘  └────┘  └─────────┘
typ        └────┘└┘└────────┘  └────┘└┘└─────────┘
doc        └────┘  └────────┘  └────┘  └─────────┘
txt        └────┘  └────────┘  └────┘  └─────────┘
par        └────┘  └────────┘  └────┘  └─────────┘
pid               └────────┘         └─────────┘
st   ───────────────────────┘└───────────────────┘└─
413        rw [← h7, ← subst_correct h2 h4], apply h3 _ h6 }
id               └┘    └───────────┘ └┘ └┘         └┘   └┘
src        └────┘  └──┘└───────────┘      └────┘  └─┘  
typ        └────┘└┘└──┘└───────────┘└┘└┘  └────┘└┘└─┘└┘
doc        └────┘  └──┘                   └────┘  └─┘  
txt        └────┘  └──┘                   └────┘  └─┘  
par        └────┘  └──┘                   └────┘  └─┘  
pid          └──┘  └──┘                          └─┘  
st   ─────────────┘└─────────────────────┘└───────────────┘└─
414     end
st   ─────┘
415  | (ee.cancel m::es) ((eq::eqs), les) h1 :=
id      └───────┘  └┘       └┘
src     └───────┘  └┘       └┘
typ     └───────┘  └┘       └┘
416    begin
st     └─────
417      unfold eq_elim,
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid            └──────┘
st   ─────────────────┘└─
418      apply sat_eq_elim,
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ────────────────────┘└─
419      cases h1 with v h1,
id             └┘
src      └────┘  └────────┘
typ      └────┘└┘└────────┘
doc      └────┘  └────────┘
txt      └────┘  └────────┘
par      └────┘  └────────┘
pid             └────────┘
st   ─────────────────────┘└─
420      existsi v,
id               
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid             
st   ────────────┘└─
421      cases h1 with h1 h2,
id             └┘
src      └────┘  └─────────┘
typ      └────┘└┘└─────────┘
doc      └────┘  └─────────┘
txt      └────┘  └─────────┘
par      └────┘  └─────────┘
pid             └─────────┘
st   ──────────────────────┘└─
422      rw list.forall_mem_cons at h1, cases h1 with h1 h3,
id          └──────────────────┘              └┘
src      └─┘└──────────────────┘└────┘  └────┘  └─────────┘
typ      └─┘└──────────────────┘└────┘  └────┘└┘└─────────┘
doc      └─┘                    └────┘  └────┘  └─────────┘
txt      └─┘                    └────┘  └────┘  └─────────┘
par      └─┘                    └────┘  └────┘  └─────────┘
pid                            └────┘         └─────────┘
st   ────────────────────────────────┘└───────────────────┘└─
423      constructor; intros t h4; rw list.mem_map at h4;
id                                    └──────────┘
src      └─────────┘  └─────────┘  └─┘└──────────┘└────┘
typ      └─────────┘  └─────────┘  └─┘└──────────┘└────┘
doc      └─────────┘  └─────────┘  └─┘            └────┘
txt      └─────────┘  └─────────┘  └─┘            └────┘
par      └─────────┘  └─────────┘  └─┘            └────┘
pid                         └───┘                └────┘
st   ────────────────────────────────┘└──────────┘└───────
424      rcases h4 with ⟨s,h4,h5⟩; rw ← h5;
id              └┘                      └┘
src      └─────┘  └─────────────┘  └───┘
typ      └─────┘└┘└─────────────┘  └───┘└┘
doc      └─────┘  └─────────────┘  └───┘
txt      └─────┘  └─────────────┘  └───┘
par      └─────┘  └─────────────┘  └───┘
pid              └─────────────┘    └─┘
st   ───────────────────────────────────────
425      simp only [term.val_add, term.val_mul, cancel];
id                  └──────────┘  └──────────┘  └────┘
src      └─────────┘└──────────┘└┘└──────────┘└┘└────┘
typ      └─────────┘└──────────┘└┘└──────────┘└┘└────┘
doc      └─────────┘            └┘            └┘      
txt      └─────────┘            └┘            └┘      
par      └─────────┘            └┘            └┘      
pid          └──┘└┘            └┘            └┘      
st   ────────────────────────────────────────────────────
426      rw [← h1, mul_zero, zero_add],
id             └┘  └──────┘  └──────┘
src      └────┘  └┘└──────┘└┘└──────┘
typ      └────┘└┘└┘└──────┘└┘└──────┘
doc      └────┘  └┘        └┘        
txt      └────┘  └┘        └┘        
par      └────┘  └┘        └┘        
pid        └──┘  └┘        └┘        
st   ───────┘└──┘└────────┘└────────┘└─
427      { apply h3 _ h4 },
id               └┘   └┘
src        └────┘  └─┘  
typ        └────┘└┘└─┘└┘
doc        └────┘  └─┘  
txt        └────┘  └─┘  
par        └────┘  └─┘  
pid               └─┘  
st   ─────┘└────────────┘└┘
428      { apply h2 _ h4 }
id               └┘   └┘
src        └────┘  └─┘  
typ        └────┘└┘└─┘└┘
doc        └────┘  └─┘  
txt        └────┘  └─┘  
par        └────┘  └─┘  
pid               └─┘  
st   ───────────────────┘└─
429    end
st   ────┘
430  
431  lemma unsat_of_unsat_eq_elim (ee : list ee) (c : clause) :
id                                      └──┘ └┘       └────┘
src                                     └──┘ └┘       └────┘
typ                                     └──┘ └┘       └────┘
432    (eq_elim ee c).unsat → c.unsat :=
id      └─────┘ └┘  └───┘    └────┘
src     └─────┘      └───┘     └────┘
typ     └─────┘ └┘  └───┘    └────┘
433  by {intros h1 h2, apply h1, apply sat_eq_elim h2}
id                                     └─────────┘ └┘
src      └──────────┘  └────┘    └────┘└─────────┘
typ      └──────────┘  └────┘    └────┘└─────────┘└┘
doc      └──────────┘  └────┘    └────┘           
txt      └──────────┘  └────┘    └────┘           
par      └──────────┘  └────┘    └────┘           
pid            └────┘                           
st     └────────────┘└────────┘└────────────────────┘└┘
434  
435  end omega